Further Reading and Links
Textbook
Textbook about programming language semantics and proof in Isabelle. We will mainly use the first part about proof in Isabelle, and some of the later chapters on program verification.
Further Reading
Documentation and publications that go deeper into the topics covered in the lecture.
- Tobias Nipkow, Lawrence C. Paulson,
Markus Wenzel: Isabelle/HOL - A
Proof Assistant for Higher-Order Logic, LNCS 2283,
Springer, 2002.
This is the old official Isabelle tutorial. It explains some Isabelle topics in more detail. -
Isabelle system and reference
documentation.
Everything about Isabelle in full gory detail. - Apostolos Doxiadis, Christos H. Papadimitriou, Alecos Papadatos, Annie Di Donna. Logicomix: An Epic Search for Truth. 2009
- Hendrik Pieter Barendregt. The Lambda Calculus, its Syntax and Semantics, North-Holland, 2nd edition, 1984.
- Chris Hankin. Lambda Calculi. A Guide for Computer Scientists, Oxford University Press, 1994.
- Tobias Nipkow, Functional Unification of Higher-Order Patterns, In: Proc. 8th IEEE Symp. Logic in Computer Science, p. 64-74, 1993.
- Wolfgang Naraschewski and Tobias Nipkow, Type Inference Verified: Algorithm W in Isabelle/HOL, Journal of Automated Reasoning, volume 23, p. 299-318, 1999.
- Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56 68, 1940. doi:10.2307/2266170
- Michael J. C. Gordon and Tom F. Melham (eds), Introduction to HOL. Cambridge University Press, 1993.
- Jeremy Avigad and Richard Zach, The Epsilon Calculus, The Stanford Encyclopedia of Philosophy (Summer 2002 Edition), Edward N. Zalta (ed.), 2002.
- Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.
- Jeremy Avigad. Mathematical method and proof. 2004.
- Elsa L. Gunter. Why we can't have SML style datatype declarations in HOL. In L. J. M. Claese and M. J. C. Gordon, editors, Higher Order Logic Theorem Proving and Its Applications, volume A-20 of IFIP Transactions, pages 561-568. North-Holland Press, September 1992.
- Stefan Berghofer and Markus Wenzel. Inductive datatypes in HOL - lessons learned in Formal-Logic Engineering. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, L. Théry, editors, TPHOLs'99, LNCS 1690. Springer-Verlag 1999.
- John Harrison. Inductive definitions: automation and application. Proceedings of the 1995 International Workshop on Higher Order Logic theorem proving and its applications, Aspen Grove, Utah, 1995. Springer LNCS 971, pp. 200-213, 1995.
- Hanne Riis Nielson, Flemming Nielson. Semantics with Applications: A Formal Introduction. 1999.
Links
Tools and websites mentioned in the lecture.