diff --git a/thys/AutoFocus-Stream/document/root.tex b/thys/AutoFocus-Stream/document/root.tex --- a/thys/AutoFocus-Stream/document/root.tex +++ b/thys/AutoFocus-Stream/document/root.tex @@ -1,65 +1,65 @@ \documentclass[11pt,a4paper]{article} \usepackage{graphicx} \usepackage{isabelle,isabellesym} \usepackage{amssymb} \usepackage{wasysym} -\usepackage[latin1]{inputenc} +\usepackage[utf8]{inputenc} \usepackage[only,bigsqcap]{stmaryrd} %\usepackage{masmath} % this should be the last package used \usepackage{pdfsetup} \newcommand{\isasymNoMsg}{\ensuremath\varepsilon} %\newcommand{\isasymMsg}{\texttt{Msg}} %\newcommand{\isasymMsg}{\isatext{\rm\sffamily{}Msg}} \newcommand{\isasymMsg}{\textsf{Msg}} % \newcommand{\isasymB}{\textsf{B}} % \newcommand{\isasymR}{\textsf{R}} % \newcommand{\isasymS}{\textsf{S}} % \newcommand{\isasymU}{\textsf{U}} % \newcommand{\isasymW}{\textsf{W}} \newcommand{\backslashlessgreater}[1]{\ensuremath{\backslash\!\!<}#1\ensuremath{>}} \newcommand{\isasymHTMLNoMsg}{\backslashlessgreater{HTMLNoMsg}} \newcommand{\isasymHTMLMsg}{\backslashlessgreater{HTMLMsg}} \urlstyle{rm} \isabellestyle{it} \pagestyle{myheadings} \begin{document} \title{AutoFocus Stream Processing for Single-Clocking and Multi-Clocking Semantics} \author{David Trachtenherz} \maketitle \begin{abstract} We formalize the AutoFocus Semantics (a time-synchronous subset of the Focus formalism) as stream processing functions on finite and infinite message streams represented as finite/infinite lists. The formalization comprises both the conventional single-clocking semantics (uniform global clock for all components and communications channels) and its extension to multi-clocking semantics (internal execution clocking of a component may be a multiple of the external communication clocking). The semantics is defined by generic stream processing functions making it suitable for simulation/code generation in Isabelle/HOL. Furthermore, a number of AutoFocus semantics properties are formalized using definitions from the Nat-Interval-Logic theories. \end{abstract} \tableofcontents \begin{center} \includegraphics[scale=0.5]{session_graph} \end{center} \clearpage \parindent 0pt\parskip 0.5ex \input{session} \end{document} diff --git a/thys/CCS/document/root.tex b/thys/CCS/document/root.tex --- a/thys/CCS/document/root.tex +++ b/thys/CCS/document/root.tex @@ -1,63 +1,63 @@ \documentclass[11pt,a4paper]{article} \usepackage{isabelle,isabellesym} \usepackage{amssymb} \usepackage[english]{babel} -\usepackage[latin1]{inputenc} +\usepackage[utf8]{inputenc} % this should be the last package used \usepackage{pdfsetup} % urls in roman style, theory text in math-similar italics \urlstyle{rm} \isabellestyle{it} \begin{document} \title{The Calculus of Communicating Systems} \author{Jesper Bengtson} \maketitle \begin{abstract} We formalise a large portion of CCS as described in Milner's book 'Communication and Concurrency' using the nominal datatype package in Isabelle. Our results include many of the standard theorems of bisimulation equivalence and congruence, for both weak and strong versions. One main goal of this formalisation is to keep the machine-checked proofs as close to their pen-and-paper counterpart as possible. \end{abstract} \tableofcontents \section{Overview} These theories formalise the following results from Milner's book Communication and Concurrency. \begin{itemize} \item strong bisimilarity is a congruence \item strong bisimilarity respects the laws of structural congruence \item weak bisimilarity is preserved by all operators except sum \item weak congruence is a congruence \item all strongly bisimilar agents are also weakly congruent which in turn are weakly bisimilar. As a corollary, weak bisimilarity and weak congruence respect the laws of structural congruence. \end{itemize} The file naming convention is hopefully self explanatory, where the prefixes \emph{Strong} and \emph{Weak} denote that the file covers theories required to formalise properties of strong and weak bisimilarity respectively; if the file name contains \emph{Sim} the theories cover simulation, file names containing \emph{Bisim} cover bisimulation, and file names containing \emph{Cong} cover weak congruence; files with the suffix \emph{Pres} deal with theories that reason about preservation properties of operators such as a certain simulation or bisimulation being preserved by a certain operator; files with the suffix \emph{SC} reason about structural congruence. For a complete exposition of all theories, please consult Bengtson's Ph. D. thesis \cite{bengtson:thesis}. % include generated text of all theories \section{Formalisation} \input{session} \bibliographystyle{abbrv} \bibliography{root} \end{document} diff --git a/thys/Group-Ring-Module/document/root.tex b/thys/Group-Ring-Module/document/root.tex --- a/thys/Group-Ring-Module/document/root.tex +++ b/thys/Group-Ring-Module/document/root.tex @@ -1,34 +1,34 @@ \documentclass[11pt,a4paper]{report} \usepackage{isabelle,isabellesym} \usepackage{amssymb} \usepackage[english]{babel} -\usepackage[latin1]{inputenc} +\usepackage[utf8]{inputenc} % this should be the last package used \usepackage{pdfsetup} % urls in roman style, theory text in math-similar italics \urlstyle{rm} \isabellestyle{it} \begin{document} \title{Group Ring Module} \author{Hidetsune Kobayashi, L. Chen, H. Murao} \maketitle \begin{abstract} The theory of groups, rings and modules is developed to a great depth. Group theory results include Zassenhaus's theorem and the Jordan-Hoelder theorem. The ring theory development includes ideals, quotient rings and the Chinese remainder theorem. The module development includes the Nakayama lemma, exact sequences and Tensor products. \end{abstract} \tableofcontents % include generated text of all theories \input{session} \end{document} diff --git a/thys/HOL-CSP/document/root.tex b/thys/HOL-CSP/document/root.tex --- a/thys/HOL-CSP/document/root.tex +++ b/thys/HOL-CSP/document/root.tex @@ -1,63 +1,63 @@ \documentclass[11pt,a4paper]{book} \usepackage{isabelle,isabellesym} \usepackage{graphicx} \graphicspath {{figures/}} % further packages required for unusual symbols (see also % isabellesym.sty), use only when needed \usepackage{latexsym} \usepackage{amssymb} %for \, \, \, \, \, \, %\, \, \, \, \, %\, \, \ %\usepackage[greek,english]{babel} %option greek for \ %option english (default language) for \, \ -%\usepackage[latin1]{inputenc} +%\usepackage[utf8]{inputenc} %for \, \, \, \, %\, \, \ %\usepackage[only,bigsqcap]{stmaryrd} %for \ %\usepackage{eufrak} %for \ ... \, \ ... \ (also included in amssymb) %\usepackage{textcomp} %for \, \ % this should be the last package used \usepackage{pdfsetup} % urls in roman style, theory text in math-similar italics \urlstyle{rm} \isabellestyle{it} \begin{document} \title{HOL-CSP Version 2.0} \author{ Safouan Taha \and Burkhart Wolff \and Lina Ye } \maketitle \tableofcontents % sane default for proof documents \parindent 0pt\parskip 0.5ex % generated text of all theories \input{session} % optional bibliography \bibliographystyle{abbrv} \bibliography{adb-long,root} \end{document} %%% Local Variables: %%% mode: latex %%% TeX-master: t %%% End: diff --git a/thys/LatticeProperties/document/root.tex b/thys/LatticeProperties/document/root.tex --- a/thys/LatticeProperties/document/root.tex +++ b/thys/LatticeProperties/document/root.tex @@ -1,67 +1,67 @@ \documentclass[11pt,a4paper]{article} \usepackage{isabelle,isabellesym} \usepackage{amssymb} -\usepackage[latin1]{inputenc} +\usepackage[utf8]{inputenc} \usepackage[only,bigsqcap]{stmaryrd} % this should be the last package used \usepackage{pdfsetup} % urls in roman style, theory text in math-similar italics \urlstyle{rm} \isabellestyle{it} \begin{document} \title{Lattice Properties} \author{Viorel Preoteasa} \maketitle \begin{abstract} This formalization introduces and collects some algebraic structures based on lattices and complete lattices for use in other developments. The structures introduced are modular, and lattice ordered groups. In addition to the results proved for the new lattices, this formalization also introduces theorems about latices and complete lattices in general. \end{abstract} \tableofcontents \parindent 0pt\parskip 0.5ex \section{Overview} Section 2 introduces well founded and transitive relations. Section 3 introduces some properties about fixpoints of monotonic application which maps monotonic functions to monotonic functions. The most important property is that such a monotonic application has the least fixpoint monotonic. Section 4 introduces conjunctive, disjunctive, universally conjunctive, and universally disjunctive functions. In section 5 some simplification lemmas for alttices are proved. Section 6 introduces modular lattices and proves some properties about them and about distributive lattices. The main result of this section is that a lattice is distributive if and only if it satisfies $$\forall x \; y \; z: x \sqcap z = y \sqcap z \land x \sqcup z = y \sqcup z \longrightarrow x = y$$ Section 7 introduces lattice ordered groups and some of their properties. The most important is that they are distributive lattices, and this property is proved using the results from Section 5. % generated text of all theories \input{session} % optional bibliography \bibliographystyle{abbrv} \bibliography{root} \end{document} %%% Local Variables: %%% mode: latex %%% TeX-master: t %%% End: diff --git a/thys/List-Infinite/document/root.tex b/thys/List-Infinite/document/root.tex --- a/thys/List-Infinite/document/root.tex +++ b/thys/List-Infinite/document/root.tex @@ -1,43 +1,43 @@ \documentclass[11pt,a4paper]{article} \usepackage{graphicx} \usepackage{isabelle,isabellesym} \usepackage{amssymb} -\usepackage[latin1]{inputenc} +\usepackage[utf8]{inputenc} \usepackage[only,bigsqcap]{stmaryrd} %\usepackage{masmath} % this should be the last package used \usepackage{pdfsetup} \urlstyle{rm} \isabellestyle{it} \pagestyle{myheadings} \begin{document} \title{Infinite Lists} \author{David Trachtenherz} \maketitle \begin{abstract} We introduce a theory of infinite lists in HOL formalized as functions over naturals (folder ListInf, theories ListInf and ListInf\_Prefix). It also provides additional results for finite lists (theory ListInf/List2), natural numbers (folder CommonArith, esp. division/modulo, naturals with infinity), sets (folder CommonSet, esp. cutting/truncating sets, traversing sets of naturals). \end{abstract} \tableofcontents \begin{center} \includegraphics[scale=0.5]{session_graph} \end{center} \clearpage \parindent 0pt\parskip 0.5ex \input{session} \end{document} diff --git a/thys/LocalLexing/document/root.tex b/thys/LocalLexing/document/root.tex --- a/thys/LocalLexing/document/root.tex +++ b/thys/LocalLexing/document/root.tex @@ -1,37 +1,37 @@ \documentclass[11pt,a4paper]{article} \usepackage{graphicx} \usepackage{isabelle,isabellesym} \usepackage{amssymb} -\usepackage[latin1]{inputenc} +\usepackage[utf8]{inputenc} \usepackage{url} % this should be the last package used \usepackage{pdfsetup} \urlstyle{rm} \isabellestyle{it} \pagestyle{myheadings} \begin{document} \title{Local Lexing} \author{Steven Obua} \maketitle \begin{abstract} This formalisation accompanies the paper Local Lexing\footnote{\url{https://arxiv.org/abs/1702.03277}}, which introduces a novel parsing concept of the same name. The paper also gives a high-level algorithm for local lexing as an extension of Earley's algorithm. This formalisation proves the algorithm to be correct with respect to its local lexing semantics. As a special case, this formalisation thus also contains a proof of the correctness of Earley's algorithm. The paper contains a short outline of how this formalisation is organised. \end{abstract} \tableofcontents \begin{center} \includegraphics[scale=0.5]{session_graph} \end{center} \clearpage \parindent 0pt\parskip 0.5ex \input{session} \end{document} diff --git a/thys/Nat-Interval-Logic/document/root.tex b/thys/Nat-Interval-Logic/document/root.tex --- a/thys/Nat-Interval-Logic/document/root.tex +++ b/thys/Nat-Interval-Logic/document/root.tex @@ -1,63 +1,63 @@ \documentclass[11pt,a4paper]{article} \usepackage{graphicx} \usepackage{isabelle,isabellesym} \usepackage{amssymb} \usepackage{wasysym} -\usepackage[latin1]{inputenc} +\usepackage[utf8]{inputenc} \usepackage[only,bigsqcap]{stmaryrd} %\usepackage{masmath} % this should be the last package used \usepackage{pdfsetup} \newcommand{\isasymNoMsg}{\ensuremath\varepsilon} %\newcommand{\isasymMsg}{\texttt{Msg}} %\newcommand{\isasymMsg}{\isatext{\rm\sffamily{}Msg}} \newcommand{\isasymMsg}{\textsf{Msg}} % \newcommand{\isasymB}{\textsf{B}} % \newcommand{\isasymR}{\textsf{R}} % \newcommand{\isasymS}{\textsf{S}} % \newcommand{\isasymU}{\textsf{U}} % \newcommand{\isasymW}{\textsf{W}} \newcommand{\backslashlessgreater}[1]{\ensuremath{\backslash\!\!<}#1\ensuremath{>}} \newcommand{\isasymHTMLNoMsg}{\backslashlessgreater{HTMLNoMsg}} \newcommand{\isasymHTMLMsg}{\backslashlessgreater{HTMLMsg}} \urlstyle{rm} \isabellestyle{it} \pagestyle{myheadings} \begin{document} \title{Interval Temporal Logic on Natural Numbers} \author{David Trachtenherz} \maketitle \begin{abstract} We introduce a theory of temporal logic operators using sets of natural numbers as time domain, formalized in a shallow embedding manner. The theory comprises special natural intervals (theory IL\_Interval: open and closed intervals, continuous and modulo intervals, interval traversing results), operators for shifting intervals to left/right on the number axis as well as expanding/contracting intervals by constant factors (theory IL\_IntervalOperators.thy), and ultimately definitions and results for unary and binary temporal operators on arbitrary natural sets (theory IL\_TemporalOperators). \end{abstract} \tableofcontents \begin{center} \includegraphics[scale=0.5]{session_graph} \end{center} \clearpage \parindent 0pt\parskip 0.5ex \input{session} \end{document} diff --git a/thys/Pi_Calculus/document/root.tex b/thys/Pi_Calculus/document/root.tex --- a/thys/Pi_Calculus/document/root.tex +++ b/thys/Pi_Calculus/document/root.tex @@ -1,82 +1,82 @@ \documentclass[11pt,a4paper]{article} \usepackage{isabelle,isabellesym} \usepackage{amssymb} \usepackage[english]{babel} -\usepackage[latin1]{inputenc} +\usepackage[utf8]{inputenc} % this should be the last package used \usepackage{pdfsetup} % urls in roman style, theory text in math-similar italics \urlstyle{rm} \isabellestyle{it} \begin{document} \title{The pi-calculus} \author{Jesper Bengtson} \maketitle \begin{abstract} We formalise the pi-calculus using the nominal datatype package, based on ideas from the nominal logic by Pitts et al., and demonstrate an implementation in Isabelle/HOL. The purpose is to derive powerful induction rules for the semantics in order to conduct machine checkable proofs, closely following the intuitive arguments found in manual proofs. In this way we have covered many of the standard theorems of bisimulation equivalence and congruence, both late and early, and both strong and weak in a uniform manner. We thus provide one of the most extensive formalisations of a the pi-calculus ever done inside a theorem prover. A significant gain in our formulation is that agents are identified up to alpha-equivalence, thereby greatly reducing the arguments about bound names. This is a normal strategy for manual proofs about the pi-calculus, but that kind of hand waving has previously been difficult to incorporate smoothly in an interactive theorem prover. We show how the nominal logic formalism and its support in Isabelle accomplishes this and thus significantly reduces the tedium of conducting completely formal proofs. This improves on previous work using weak higher order abstract syntax since we do not need extra assumptions to filter out exotic terms and can keep all arguments within a familiar first-order logic. \end{abstract} \tableofcontents \section{Overview} The following results of the pi-calculus meta-theory are formalised, where the notation (e) means that the results cover the early operational semantics and (l) the late one. \begin{itemize} \item strong bisimilarity is preserved by all operators except the input-prefix (e/l) \item strong equivalence is a congruence (e/l) \item weak bisimilarity is preserved by all operators except the input-prefix and sum (e/l) \item weak congruence is a congruence (e/l) \item strong equivalence respect the laws of structural congruence (l) \item all strongly equivalent agents are also weakly congruent which in turn are weakly bisimilar. Moreover, strongly equivalent agents are also strongly bisimilar (e/l) \item all late equivalences are included in their early counterparts. \item as a corollary of the last three points, all mentioned equivalences respect the laws of structural congruence \item the axiomatisation of the finite fragment of strong late bisimilarity is sound and complete \item The Hennessy lemma (l) \end{itemize} The file naming convention is hopefully self-explanatory, where the prefixes \emph{Strong} and \emph{Weak} denote that the file covers theories required to formalise properties of strong and weak bisimilarity respectively; if the file name contians \emph{Early} or \emph{Late} the theories work with the early or the late operational semantics of the pi-calculus respectively; if the file name contains \emph{Sim} the theories cover simulation, file names containing \emph{Bisim} cover bisimulation, and file names containing \emph{Cong} cover weak congruence; files with the suffix \emph{Pres} deal with theories that reason about preservation properties of operators such as a certain simulation or bisimulation being preserved by a certain operator; files with the suffix \emph{SC} reason about structural congruence. For a complete exposition of all of theories, please consult Bengtson's Ph. D. thesis \cite{bengtson:thesis}. A shorter presentation can be found in our LMCS article 'Formalising the pi-calculus using nominal logic' from 2009 \cite{bengtson:lmcs09}. A recollection of the axiomatisation results can be found in the SOS article 'A completeness proof for bisimulation in the pi-calculus using Isabelle' from 2007 \cite{bengtson:sos07}. % include generated text of all theories \section{Formalisation} \input{session} \bibliographystyle{abbrv} \bibliography{root} \end{document} diff --git a/thys/Probabilistic_Noninterference/document/root.tex b/thys/Probabilistic_Noninterference/document/root.tex --- a/thys/Probabilistic_Noninterference/document/root.tex +++ b/thys/Probabilistic_Noninterference/document/root.tex @@ -1,59 +1,59 @@ \documentclass[11pt,a4paper]{article} \usepackage{isabelle,isabellesym} \usepackage{amssymb} -\usepackage[latin1]{inputenc} +\usepackage[utf8]{inputenc} \usepackage[only,bigsqcap]{stmaryrd} % this should be the last package used \usepackage{pdfsetup} \usepackage{hyperref} % urls in roman style, theory text in math-similar italics \urlstyle{rm} \isabellestyle{it} \begin{document} \title{Probabilistic Noninterference} \author{Andrei Popescu \hspace*{10ex} Johannes H\"{o}lzl} \maketitle \begin{abstract} We formalize a probabilistic noninterference for a multi-threaded language with uniform scheduling, where probabilistic behaviour comes from both the scheduler and the individual threads. We define notions probabilistic noninterference in two variants: resumption-based and trace-based. For the resumption-based notions, we prove compositionality w.r.t.\ the language constructs and establish sound type-system-like syntactic criteria. This is a formalization of the mathematical development presented in the papers~\cite{cpp2013,calco2013}. It is the probabilistic variant of the \href{http://isa-afp.org/entries/Possibilistic_Noninterference.shtml}{Possibilistic Noninterference} AFP entry. \end{abstract} \tableofcontents % sane default for proof documents \parindent 0pt\parskip 0.5ex % generated text of all theories \input{session} % optional bibliography \bibliographystyle{abbrv} \bibliography{root} \end{document} %%% Local Variables: %%% mode: latex %%% TeX-master: t %%% End: diff --git a/thys/PseudoHoops/document/root.tex b/thys/PseudoHoops/document/root.tex --- a/thys/PseudoHoops/document/root.tex +++ b/thys/PseudoHoops/document/root.tex @@ -1,63 +1,63 @@ \documentclass[11pt,a4paper]{article} \usepackage{isabelle,isabellesym} -\usepackage[latin1]{inputenc} +\usepackage[utf8]{inputenc} \usepackage[only,bigsqcap]{stmaryrd} % this should be the last package used \usepackage{pdfsetup} % urls in roman style, theory text in math-similar italics \urlstyle{rm} \isabellestyle{it} \begin{document} \title{Pseudo-hoops} \author{George Georgescu and Lauren\c tiu Leu\c stean and Viorel Preoteasa} \maketitle \begin{abstract} Pseudo-hoops are algebraic structures introduced in \cite{bosbach:1969,bosbach:1970} by B. Bosbach under the name of complementary semigroups. This is a formalization of the paper \cite{georgescu:leustean:preoteasa:2005}. Following \cite{georgescu:leustean:preoteasa:2005} we prove some properties of pseudo-hoops and we define the basic concepts of filter and normal filter. The lattice of normal filters is isomorphic with the lattice of congruences of a pseudo-hoop. We also study some important classes of pseudo-hoops. Bounded Wajsberg pseudo-hoops are equivalent to pseudo-Wajsberg algebras and bounded basic pseudo-hoops are equiv- alent to pseudo-BL algebras. Some examples of pseudo-hoops are given in the last section of the formalization. \end{abstract} \tableofcontents \section{Overview} Section 2 introduces some operations and their infix syntax. Section 3 and 4 introduces some facts about residuated and complemented monoids. Section 5 introduces the pseudo-hoops and some of their properties. Section 6 introduces filters and normal filters and proves that the lattice of normal filters and the lattice of congruences are isomorphic. Following \cite{ceterchi:2001}, section 7 introduces pseudo-Waisberg algebras and some of their properties. In Section 8 we investigate some classes of pseudo-hoops. Finally section 9 presents some examples of pseudo-hoops and normal filters. \parindent 0pt\parskip 0.5ex % generated text of all theories \input{session} % optional bibliography \bibliographystyle{abbrv} \bibliography{root} \end{document} %%% Local Variables: %%% mode: latex %%% TeX-master: t %%% End: diff --git a/thys/Psi_Calculi/document/root.tex b/thys/Psi_Calculi/document/root.tex --- a/thys/Psi_Calculi/document/root.tex +++ b/thys/Psi_Calculi/document/root.tex @@ -1,79 +1,79 @@ \documentclass[11pt,a4paper]{article} \usepackage{isabelle,isabellesym} \usepackage{amssymb} \usepackage[english]{babel} -\usepackage[latin1]{inputenc} +\usepackage[utf8]{inputenc} % this should be the last package used \usepackage{pdfsetup} % urls in roman style, theory text in math-similar italics \urlstyle{rm} \isabellestyle{it} \begin{document} \title{The pi-calculus} \author{Jesper Bengtson} \maketitle \begin{abstract} \end{abstract} \tableofcontents \section{Overview} These theories formalise the following results for psi-calculi. Note that there is only an early semantics for psi-calculi, although a late one may appear later. \begin{itemize} \item strong bisimilarity is preserved by all operators except the input-prefix \item strong equivalence is a congruence \item weak bisimilarity is preserved by all operators except case and the input-prefix \item weak congruence is a congruence \item strong equivalence respect the laws of structural congruence \item all strongly equivalent agents are also weakly congruent which in turn are weakly bisimilar. Moreover, strongly equivalent agents are also strongly bisimilar \item as a corollary of the last two points, all mentioned equivalences respect the law of structural congruence \item for instances of psi-calculi where assertion composition satisfies weakening, the definition of weak bisimilarity can be simplified significantly and proven equivalent to the version that applies when weakening does not hold \item for certain versions of psi-calculi, sum can be encoded \item for certain versions of psi-calculi, the tau-prefix can be encoded and when weakening is satisfied, all of the tau-laws hold. \end{itemize} The file naming convention is hopefully self explanatory, where the prefixes \emph{Strong} and \emph{Weak} denote that the file covers theories required to formalise properties of strong and weak bisimilarity respectively; files with the prefix \emph{Weaken} cover theories where weakening holds for the static implication; if the file name contains \emph{Sim} the theories cover simulation, file names containing \emph{Bisim} cover bisimulation, and file names containing \emph{Cong} cover weak congruence; files with the suffix \emph{Pres} deal with theories that reason about preservation properties of operators such as a simulation or bisimulation being preserved by a certain operator; files with the suffix \emph{StructCong} reason about structural congruence. For a complete exposition of all of theories, please consult Bengtson's Ph. D. thesis \cite{bengtson:thesis}. A shorter presentation can be found in our TPHOLs paper 'Psi-calculi in Isabelle' from 2009 \cite{bengtson:tphols09}. There are also two LICS-papers that focus on the mathematical theories, rather than the Isabelle formalisations \cite{bengtson:lics09, johansson:lics10}. % include generated text of all theories \section{Formalisation} \input{session} \bibliographystyle{abbrv} \bibliography{root} \end{document} diff --git a/thys/RefinementReactive/document/root.tex b/thys/RefinementReactive/document/root.tex --- a/thys/RefinementReactive/document/root.tex +++ b/thys/RefinementReactive/document/root.tex @@ -1,98 +1,98 @@ \documentclass[11pt,a4paper]{article} \usepackage{isabelle,isabellesym} \usepackage{amssymb} \usepackage{wasysym} -\usepackage[latin1]{inputenc} +\usepackage[utf8]{inputenc} \usepackage[only,bigsqcap]{stmaryrd} % this should be the last package used \usepackage{pdfsetup} \newcommand{\tv}{{\isacharprime}\,} % urls in roman style, theory text in math-similar italics \urlstyle{rm} \isabellestyle{it} \begin{document} \title{Formalization of Refinement Calculus for Reactive Systems} \author{Viorel Preoteasa\\ Aalto University, Finland} \maketitle \begin{abstract} We present a formalization of refinement calculus for reactive systems. Refinement calculus is based on monotonic predicate transformers (monotonic functions from sets of post-states to sets of pre-states), and it is a powerful formalism for reasoning about imperative programs. We model reactive systems as monotonic property transformers that transform sets of output infinite sequences into sets of input infinite sequences. Within this semantics we can model refinement of reactive systems, (unbounded) angelic and demonic nondeterminism, sequential composition, and other semantic properties. We can model systems that may fail for some inputs, and we can model compatibility of systems. We can specify systems that have liveness properties using linear temporal logic, and we can refine system specifications into systems based on symbolic transitions systems, suitable for implementations. \end{abstract} \tableofcontents \parindent 0pt\parskip 0.5ex \section{Introduction} This is a formalization of refinement calculus for reactive systems that is presented in \cite{preoteasa:tripakis:2014tr}. Refinement calculus \cite{back-1978,back-wright-98} has been developed originally for input output imperative programs, and is based on a predicate transformer semantics of programs with a weakest precondition interpretation. We extend the standard refinement calculus to reactive systems \cite{Harel:1989:DRS:101969.101990}. Within our framework a reactive system is seen as a system that accepts as input an infinite sequence of values and productes as output an infinite sequence of values. The semantics of these systems is given as {\em monotonic property transformers}. These are monotonic functions which maps sets of output sequences (output properties) into sets of input sequences (input properties). For a set of output sequences $q$, the monotonic property transformer $S$ applied to $q$ returns all input sequences from which the computation of $S$ always produces a sequence from $q$. Our work extends also the relational interfaces framework of \cite{tripakis:2011} which can handle only finite safety properties to infinite properties and liveness. This formalization is organized in three sections. Section 2 presents an algebraic formalization of linear temporal locic. Section 3 introduces basic constructs from refinement calculus, and finally Section 4 applies the refinement calculus to reactive systems. % generated text of all theories \input{session} % optional bibliography \bibliographystyle{abbrv} \bibliography{root} \end{document} %%% Local Variables: %%% mode: latex %%% TeX-master: t %%% End: diff --git a/thys/Security_Protocol_Refinement/document/root.tex b/thys/Security_Protocol_Refinement/document/root.tex --- a/thys/Security_Protocol_Refinement/document/root.tex +++ b/thys/Security_Protocol_Refinement/document/root.tex @@ -1,164 +1,164 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % Project: Development of Security Protocols by Refinement % % Module: document/session_graph.tex (Isabelle/HOL 2016-1) % ID: $Id: root.tex 134929 2017-05-24 18:27:58Z csprenge $ % Author: Christoph Sprenger, ETH Zurich % % session graph for PDF document % % Copyright (c) 2009-2017 Christoph Sprenger % Licence: LGPL % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \documentclass[11pt,a4paper]{report} \usepackage{isabelle,isabellesym} % input user-defined stuff \usepackage{a4wide} \input{isapreamble.tex} % further packages required for unusual symbols (see also % isabellesym.sty), use only when needed %\usepackage{amssymb} %for \, \, \, \, \, \, %\, \, \, \, \, %\, \, \ %\usepackage[greek,english]{babel} %option greek for \ %option english (default language) for \, \ -%\usepackage[latin1]{inputenc} +%\usepackage[utf8]{inputenc} %for \, \, \, \, %\, \, \ %\usepackage[only,bigsqcap]{stmaryrd} %for \ %\usepackage{eufrak} %for \ ... \, \ ... \ (also included in amssymb) %\usepackage{textcomp} %for \, \ % this should be the last package used \usepackage{pdfsetup} % urls in roman style, theory text in math-similar italics \urlstyle{rm} \isabellestyle{it} \begin{document} \title{Development of Security Protocols by Refinement} \author{Christoph Sprenger and Ivano Somaini \\[.5ex] ETH Zurich, Switzerland} \maketitle \begin{abstract} We propose a development method for security protocols based on stepwise refinement. Our refinement strategy transforms abstract security goals into protocols that are secure when operating over an insecure channel controlled by a Dolev-Yao-style intruder. As intermediate levels of abstraction, we employ messageless guard protocols and channel protocols communicating over channels with security properties. These abstractions provide insights on why protocols are secure and foster the development of families of protocols sharing common structure and properties. We have implemented our method in Isabelle/HOL and used it to develop different entity authentication and key establishment protocols, including realistic features such as key confirmation, replay caches, and encrypted tickets. Our development highlights that guard protocols and channel protocols provide fundamental abstractions for bridging the gap between security properties and standard protocol descriptions based on cryptographic messages. It also shows that our refinement approach scales to protocols of nontrivial size and complexity. \end{abstract} \tableofcontents % sane default for proof documents \parindent 0pt\parskip 0.5ex % display the theory dependency graph \include{session_graph} \section*{Preamble} \subsection*{Related Publications} The following papers describe our results in more detail: \begin{itemize} \item Christoph Sprenger and David Basin, \emph{Developing Security Protocols by Refinement}, CCS 2010. \item Christoph Sprenger and David Basin, \emph{Refining Key Establishment}, CSF 2012. \item Christoph Sprenger and David Basin, \emph{Refining Security Protocols}, Journal of Computer Security (in submission), 2017. \end{itemize} Note: The Isabelle/HOL sources in this distribution also include the treatment of session key compromise. This is described in our journal paper (see above), which subsumes the CCS 2010 and CSF 2012 papers. \subsection*{Mapping the model names in our papers to the Isabelle/HOL theories} For the sake of the presentation, the papers use shorter names for the models than the Isabelle theories. Here is a mapping of the names. On the left you find the model name used in the papers and on the right the corresponding Isabelle/HOL theory name. Note that the Isabelle theories contain a separate lemma or theorem for each invariant and refinement result. \begin{description} \item[Level 0] \mbox{ } \begin{verbatim} Refinement/ s0 s0g_secrecy a0n a0n_agree a0i a0i_agree \end{verbatim} \item[Level 1] \mbox{ } \begin{verbatim} Auth_simple/ a1 m1_auth Key_establish/ kt1 m1_keydist kt1in m1_keydist_iirn kt1nn m1_keydist_inrn nssk1 m1_nssk krb1 m1_kerberos ds1 m1_ds \end{verbatim} \item[Level 2] \mbox{ } \begin{verbatim} Auth_simple/ a2 m2_auth_chan c2 m2_confid_chan Key_establish/ nssk2 m2_nssk krb2 m2_kerberos ds2 m2_ds \end{verbatim} \item[Level 3] \mbox{ } \begin{verbatim} Auth_simple/ iso3 m3_sig nsl3 m3_enc Key_establish/ nssk3d m3_nssk_par nssk3 m3_nssk krb3d m3_kerberos_par krb3v m3_kerberos5 krb3iv m3_kerberos4 ds3d m3_ds_par ds3 m3_ds \end{verbatim} \end{description} % generated text of all theories \input{session} % optional bibliography \bibliographystyle{abbrv} \bibliography{root} \end{document} diff --git a/thys/Tarskis_Geometry/document/root.tex b/thys/Tarskis_Geometry/document/root.tex --- a/thys/Tarskis_Geometry/document/root.tex +++ b/thys/Tarskis_Geometry/document/root.tex @@ -1,47 +1,47 @@ \documentclass[11pt,a4paper]{article} \usepackage{isabelle,isabellesym} \usepackage{amssymb} \newcommand{\isasymcongruent}{\isamath{\equiv}} \renewcommand{\isasymequiv}{\isamath{\triangleq}} -\usepackage[latin1]{inputenc} +\usepackage[utf8]{inputenc} % this should be the last package used \usepackage{pdfsetup} % urls in roman style, theory text in math-similar italics \urlstyle{rm} \isabellestyle{it} \begin{document} \title{The independence of Tarski's Euclidean axiom} \author{T.~J.~M.~Makarios} \maketitle \begin{abstract} Tarski's axioms of plane geometry are formalized and, using the standard real Cartesian model, shown to be consistent. A substantial theory of the projective plane is developed. Building on this theory, the Klein--Beltrami model of the hyperbolic plane is defined and shown to satisfy all of Tarski's axioms except his Euclidean axiom; thus Tarski's Euclidean axiom is shown to be independent of his other axioms of plane geometry. An earlier version of this work was the subject of the author's MSc thesis \cite{makarios}, which contains natural-language explanations of some of the more interesting proofs. \end{abstract} \tableofcontents % generated text of all theories \input{session} % optional bibliography \bibliographystyle{abbrv} \bibliography{root} \end{document} %%% Local Variables: %%% mode: latex %%% TeX-master: t %%% End: