Larry Paulson's Archive Area

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 is distributed under a BSD-style open source licence.

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

tar zxf Isabelle99.tar.gz

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.

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.

These items are unsupported. But if you have any success with them, please let me know.

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 2021-02-20

Back to Larry Paulson's Home Page