1. Jasmin Christian Blanchette (2019): Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL (Invited Talk). In: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), pp. 1–13, doi:10.1145/3293880.3294087.
  2. Edsger W. Dijkstra (1989): On an exercise of Tony Hoare's. Circulated privately,
  3. John Harrison (2009): Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, doi:10.1017/CBO9780511576430.
  4. Alexander Birch Jensen, John Bruntse Larsen, Anders Schlichtkrull & Jørgen Villadsen (2018): Programming and verifying a declarative first-order prover in Isabelle/HOL. AI Communications 31(3), pp. 281–299, doi:10.3233/AIC-180764.
  5. Leslie Lamport (1993): How to write a proof. Global Analysis in Modern Mathematics, pp. 311–321. Also published in American Mathematical Monthly, 102(7):600-608, August-September 1995.
  6. Leslie Lamport (2012): How to write a 21st century proof. Journal of fixed point theory and applications 11(1), pp. 43–63, doi:10.1007/s11784-012-0071-6.
  7. Tobias Nipkow, Lawrence C. Paulson & Markus Wenzel (2002): Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science 2283. Springer, doi:10.1007/3-540-45949-9.
  8. Jørgen Villadsen, Andreas Halkjær From & Anders Schlichtkrull (2017): Natural Deduction and the Isabelle Proof Assistant. In: Pedro Quaresma & Walther Neuper: Proceedings 6th International Workshop on Theorem proving components for Educational Software (ThEdu), EPTCS 267, pp. 140–155, doi:10.4204/EPTCS.267.9.
  9. Jørgen Villadsen, Anders Schlichtkrull & Andreas Halkjær From (2018): A Verified Simple Prover for First-Order Logic. In: Boris Konev, Josef Urban & Philipp Rümmer: 6th Workshop on Practical Aspects of Automated Reasoning (PAAR), CEUR Workshop Proceedings 2162, Aachen, pp. 88–104. Available at

Comments and questions to:
For website issues: