Isabelle
Isabelle is a generic theorem prover.
New logics are introduced by specifying their syntax and rules of
inference. Proof procedures can be expressed using tactics and tacticals. The
latest version is Isabelle-99.
- Developers:
Lawrence C Paulson (University of Cambridge),
Tobias Nipkow (Technical University, Munich) and colleagues
- Contact:
Lawrence C. Paulson
Computer Laboratory
University of Cambridge
Pembroke Street
Cambridge CB2 3QG
England
Email: Larry.Paulson@cl.cam.ac.uk
- Number of Sites:
many
- Line Count:
43,000+ (excluding object-logics)
- In use:
1986-now
- Language:
Standard ML
- Compilers:
Poly/ML, Standard ML of New Jersey, ML Works
- Availability:
Isabelle is available from
Cambridge
and other mirror sites.
- Related Publications:
Documentation is included with the distribution.
Many research reports can be found on the
Projects Page.