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.

archive of past messages (current to July 2005)
The pre-Mailman archives are plain text files, one per year. One way to burst them is using the MH command inc.
2005 | 2004 | 2003 | 2002 | 2001 | 2000 | 1999 | 1998 | 1997 | 1996 | 1995 | 1994 | 1993 | 1990-92

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 set theory and induction/recursion.
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.
- A Verification Environment for ML Programs, by A. Cant and M. A. Ozols, Trusted Computer Systems Group, DSTO (1992)

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

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 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 $Date: 2004/04/20 11:41:45 $

Back to Larry Paulson's Home Page