2770 NeedhamSchroeder publickey authentication protocol~\cite{paulsonns} 
2770 NeedhamSchroeder publickey authentication protocol~\cite{paulsonns} 
2771 and the OtwayRees protocol. 
2771 and the OtwayRees 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 whilelanguage, the necessary 
2774 operational and axiomatic semantics of a simple whilelanguage, 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{nipkowIMP}. 
2778 Winskel~\cite{winskel93}. For details see~\cite{nipkowIMP}. 
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 verificationconditions. 
2781 logic, including a tactic for generating verificationconditions. 
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 MiniML and a correctness proof for its type 
2784 the core functional language MiniML and a correctness proof for its type 
2786 inference algorithm $\cal W$~\cite{milner78,nazarethnipkow}. 
2785 inference algorithm $\cal W$~\cite{milner78,nipkowW}. 
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 ChurchRosser proofs for $\beta$ 
2788 $\lambda$calculus in de~Bruijn notation and ChurchRosser proofs for $\beta$ 
2790 and $\eta$ reduction~\cite{NipkowCR}. 
2789 and $\eta$ reduction~\cite{NipkowCR}. 
2791 
2790 