Isabelle Related Material

• The Isabelle Homepage
• Isabelle for Solaris/Linux and MacOS X
• IsaMorph: Running Isabelle directly from CD (Isabelle Live CD)

• D. van Dalen: Logic and Structure. Springer-Verlag, 1980. An introductory textbook on logic
• David Basin and Seán Matthews: Logical Frameworks. In Dov Gabbay and Franz Guenthner, editors, Handbook of Philosophical Logic, second edition. Reidel, 2002.
• N.G. de Bruijn: A Survey of the Project AUTOMATH. In Essays in Combinatory Logic, Lambda Calculus, and Formalism. Academic Press, 1980.
• Robert Harper, Furio Honsell, and Gordon D. Plotkin: A Framework for Defining Logics. Journal of the ACM, 40(1):143-184, 1993.
• Arnon Avron, Furio Honsell, Ian A. Mason, and Robert Pollack: Using Typed Lambda Calculus to Implement Formal Systems on a Machine. Journal of Automated Reasoning 9(3):309-354, 1992
• Henk Barendregt: Introduction to Generalized Type Systems. Journal of Functional Programming 1(2):125-154, 1991.
• Lawrence C. Paulson: Isabelle: A Generic Theorem Prover. Springer LNCS 828, 1994.
• Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel: Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Springer LNCS 2283, 2002.
• Tobias Nipkow: Hoare Logics in Isabelle/HOL. In H. Schwichtenberg and R. Steinbrüggen, editors, Proceedings of Proof and System-Reliability, pages 341-367, Kluwer, 2002.

• Proof General
• Isabelle (Cambridge) (München). You will find lots of documentation there, including the Isabelle Reference Manual.
• Sara Kalvala: A gentle introduction to Isabelle.

• Larry Paulson: Logic and Proof. An introductory lecture on logic, mainly on syntax and semantics of propositional and first-order logic, and proof systems for those logics.
• Frank Pfenning: Automated Theorem Proving.
• Isabelle Course Material

• HOL-Z: A shallow embedding of Z into Isabelle HOL.
• HOL-OCL: A shallow embedding of OCL into Isabelle HOL.
• HOL-TestGen: Specification-based test case generation using Isabelle/HOL.
• Cryptographically Faithful Proofs of Security Protocols
• A larger list of Isabelle Projects