Computer Supported Modeling and Reasoning
Literature

Books and articles

1. D. van Dalen: Logic and Structure. Springer-Verlag, 1980. An introductory textbook on logic
2. David Basin and Seán Matthews: Logical Frameworks. In Dov Gabbay and Franz Guenthner, editors, Handbook of Philosophical Logic, second edition. Reidel, 2002.
3. N.G. de Bruijn: A Survey of the Project AUTOMATH. In Essays in Combinatory Logic, Lambda Calculus, and Formalism. Academic Press, 1980.
4. Robert Harper, Furio Honsell, and Gordon D. Plotkin: A Framework for Defining Logics. Journal of the ACM, 40(1):143-184, 1993.
5. 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
6. Henk Barendregt: Introduction to Generalized Type Systems. Journal of Functional Programming 1(2):125-154, 1991.
7. Lawrence C. Paulson: Isabelle: A Generic Theorem Prover. Springer LNCS 828, 1994.
8. Tobias Nipkow: Hoare Logics in Isabelle/HOL. Draft, 2001. To appear in proceedings of Marktobderdorf Summer School 2001.

Manuals and Tutorials

1. Proof General
2. Isabelle (Cambridge) (München). You will find lots of documentation there, in particular the
   1. Isabelle Reference Manual
   2. A tutorial introduction to Isabelle/HOL
   3. A manual of Isabelle/HOL, which explains many technical details for working with HOL
3. Sara Kalvala: A gentle introduction to Isabelle.

Related Lectures

1. 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.