• Isabelle: mailing list | reports | past releases | 1994 book
• Historical Relics

Isabelle Mailing List

Use the mailing list isabelle-users@cl.cam.ac.uk for discussing problems and results. To subscribe, contact our robot.

• Searchable Isabelle mailing list archives. Also archived on Zulip: until July 2020 • from August 2020
• The pre-2006 archives are plain text files, one per year.
  2005 | 2004 | 2003 | 2002 | 2001 | 2000 | 1999 | 1998 | 1997 | 1996 | 1995 | 1994 | 1993 | 1990-92

Isabelle Past Releases

• The latest version, separately packaged for Mac, Windows and Linux, is available from
  • Cambridge
  • Munich
  • and other mirrors
• past versions: Isabelle 2024 | Isabelle 2023 | Isabelle 2022 | Isabelle 2021-1 | Isabelle 2021 | Isabelle 2020 | Isabelle 2019 | Isabelle 2018 | Isabelle 2017 | Isabelle 2016-1 | Isabelle 2016 | Isabelle 2015 | Isabelle 2014 | Isabelle 2013-2 | Isabelle 2013-1 | Isabelle 2013 | Isabelle 2012 | Isabelle 2011-1 | Isabelle 2011 | Isabelle 2009-2 | Isabelle 2009-1 | Isabelle 2009 | Isabelle 2008 | Isabelle 2007 | Isabelle 2005 | Isabelle 2004 | Isabelle 2003 | Isabelle 2002 | Isabelle 99 revision 2 | Isabelle 99 revision 1 | Isabelle 99 | Isabelle 98 revision 1 | Isabelle 98 | Isabelle 94 revision 8 | Isabelle 94 revision 7 | Isabelle 94 revision 6 | Isabelle 94 | Isabelle 93 | Isabelle 92 | Isabelle 91 | Isabelle 90 | Isabelle 89 | Isabelle 86

To unpack a tar file such as Isabelle2024.tar.gz, use the command

tar zxf Isabelle2024.tar.gz

Isabelle Research Reports

• Larry Paulson's papers on Isabelle describe basic concepts, early experiments and proof search (the classical reasoner).
• Also available are papers on sledgehammer, describing the stages of its development at Cambridge.
• Larry Paulson has applied Isabelle to cryptographic protocols, mechanized formalised mathematics and induction/recursion.
• The first-ever Isabelle Users Workshop (1995), with some quite remarkable early papers.
• Paulson's 1996 Marktoberdorf lecture notes, Tool Support for Logics of Programs, survey the concepts underlying Isabelle through simple examples, while also describing advanced work.
• A selection of even earlier works, by students and visitors:
  • The Church-Rosser Theorem in Isabelle: A Proof Porting Experiment, by Ole Rasmussen (1995)
  • A Case Study of Co-induction in Isabelle, by Jacob Frost (1993)
  • Martin Coen's 1992 paper Interactive Program Derivation describes a predecessor of the object-logic CCL.

The First Isabelle Book

• Isabelle: A Generic Theorem Prover. By Lawrence C. Paulson, with contributions by Tobias Nipkow. Springer Lecture Notes in Computer Science 828. XVII+321 pages, 1994. Price: DM 66.00. ISBN 3-540-58244-4.
• Errata list.
• Datatypes and (Co)Inductive Definitions in Isabelle/HOL, by Tobias Nipkow and L. C. Paulson (1994). Note: this consists of sections from Isabelle's Object-Logics that could not be included in the book.

Historical Relics

• The original Edinburgh LCF.
• The theorem prover Cambridge LCF. This is a close predecessor of the Cambridge HOL system. It is documented in the book Logic and Computation by L. C. Paulson (CUP, 1987). It is coded in Franz Lisp.
• A very unusual compiler generator. It is documented in A semantics-directed compiler generator by L. C. Paulson, POPL (1982) and in my PhD Thesis. It is sometimes called PSP in the literature. It is coded in ISO Pascal.

Last modified on 2025-02-05

lp15@cam.ac.uk

Back to Larry Paulson's Home Page