doc-src/HOL/HOL.tex
 changeset 6588 6e6ca099f68f parent 6580 ff2c3ffd38ee child 6592 c120262044b6
equal inserted replaced
6587:a1bb7a7b6205 6588:6e6ca099f68f
2770 Needham-Schroeder public-key authentication protocol~\cite{paulson-ns}
2770 Needham-Schroeder public-key authentication protocol~\cite{paulson-ns}
2771 and the Otway-Rees protocol.
2771 and the Otway-Rees protocol.
2772
2772
2773 Directory \texttt{HOL/IMP} contains a formalization of various denotational,
2773 Directory \texttt{HOL/IMP} contains a formalization of various denotational,
2774 operational and axiomatic semantics of a simple while-language, the necessary
2774 operational and axiomatic semantics of a simple while-language, the necessary
2775 equivalence proofs, soundness and completeness of the Hoare rules with respect
2775 equivalence proofs, soundness and completeness of the Hoare rules with
2776 to the
2776 respect to the denotational semantics, and soundness and completeness of a
2777 denotational semantics, and soundness and completeness of a verification
2777 verification condition generator.  Much of development is taken from
2778 condition generator.  Much of development is taken from

2779 Winskel~\cite{winskel93}.  For details see~\cite{nipkow-IMP}.
2778 Winskel~\cite{winskel93}.  For details see~\cite{nipkow-IMP}.
2780
2779
2781 Directory \texttt{HOL/Hoare} contains a user friendly surface syntax for Hoare
2780 Directory \texttt{HOL/Hoare} contains a user friendly surface syntax for Hoare
2782 logic, including a tactic for generating verification-conditions.
2781 logic, including a tactic for generating verification-conditions.
2783
2782
2784 Directory \texttt{HOL/MiniML} contains a formalization of the type system of the
2783 Directory \texttt{HOL/MiniML} contains a formalization of the type system of
2785 core functional language Mini-ML and a correctness proof for its type
2784 the core functional language Mini-ML and a correctness proof for its type
2786 inference algorithm $\cal W$~\cite{milner78,nazareth-nipkow}.
2785 inference algorithm $\cal W$~\cite{milner78,nipkow-W}.
2787
2786
2788 Directory \texttt{HOL/Lambda} contains a formalization of untyped
2787 Directory \texttt{HOL/Lambda} contains a formalization of untyped
2789 $\lambda$-calculus in de~Bruijn notation and Church-Rosser proofs for $\beta$
2788 $\lambda$-calculus in de~Bruijn notation and Church-Rosser proofs for $\beta$
2790 and $\eta$ reduction~\cite{Nipkow-CR}.
2789 and $\eta$ reduction~\cite{Nipkow-CR}.
2791
2790