<html><head><!-- $Id$ --><title>Isabelle</title></head><body><h1>Isabelle </h1> <a href="http://www.in.tum.de/~isabelle/logo/"><imgsrc="isabelle.gif" width=100 align=right alt="[Isabelle logo]"></a><p><strong>Isabelle</strong> is a popular generic theorem provingenvironment developed at Cambridge University (<ahref="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>) and TUMunich (<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>).<p><ahref="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html"><imgsrc="cambridge.gif" width=145 border=0 align=rightalt="[Cambridge]"></a> <ahref="http://www.in.tum.de/~isabelle/munich.html"><imgsrc="munich.gif" width=48 border=0 align=right alt="[Munich]"></a>This page provides general information on Isabelle, more details areavailable on the local Isabelle pages at <ahref="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html">Cambridge</a>and <a href="http://www.in.tum.de/~isabelle/munich.html">Munich</a>.See there for information on projects done with Isabelle, mailing listarchives, research papers, the Isabelle bibliography, and Isabelleworkshops and courses.<h2>Obtaining Isabelle</h2>The latest version is <strong>Isabelle98-1</strong>, it is availablefrom several <a href="dist/">mirror sites</a>.<h2>What is Isabelle?</h2>Isabelle can be viewed from two main perspectives. On the one hand itmay serve as a generic framework for rapid prototyping of deductivesystems. On the other hand, major existing logics like<strong>Isabelle/HOL</strong> provide a theorem proving environmentready to use for sizable applications.<h3>Isabelle's Logics</h3>The Isabelle distribution includes a large body of object logics andother examples (see the <a href="library/">Isabelle theorylibrary</a>).<dl><dt><a href="library/HOL/"><strong>Isabelle/HOL</strong></a><dd> is aversion of classical higher-order logic resembling that of the <AHREF="http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html">HOLSystem</A>.<dt><a href="library/HOLCF/"><strong>Isabelle/HOLCF</strong></a><dd>adds Scott's Logic for Computable Functions (domain theory) to HOL.<dt><a href="library/FOL/"><strong>Isabelle/FOL</strong></a><dd>provides basic classical and intuitionistic first-order logic. It ispolymorphic.<dt><a href="library/ZF/"><strong>Isabelle/ZF</strong></a><dd> offersa formulation of Zermelo-Fraenkel set theory on top of FOL.</dl><p>Isabelle/HOL is currently the best developed object logic, includingan extensive library of (concrete) mathematics, and various packagesfor advanced definitional concepts (like (co-)inductive sets andtypes, well-founded recursion etc.). The distribution also includessome large applications, for example correctness proofs ofcryptographic protocols (<a href="library/HOL/Auth/">HOL/Auth</a>) orcommunication protocols (<a href="library/HOLCF/IOA/">HOLCF/IOA</a>).<p>Isabelle/ZF provides another starting point for applications, with aslightly less developed library. Its definitional packages aresimilar to those of Isabelle/HOL. Untyped ZF provides more advancedconstructions for sets than simply-typed HOL.<p>There are a few minor object logics that may serve as furtherexamples: <a href="library/CTT/">CTT</a> is an extensional version ofMartin-Löf's Type Theory, <a href="library/Cube/">Cube</a> isBarendregt's Lambda Cube. There are also some sequent calculusexamples under <a href="library/Sequents/">Sequents</a>, includingmodal and linear logics. Again see the <a href="library/">Isabelletheory library</a> for other examples.<h3>Defining Logics</h3>Logics are not hard-wired into Isabelle, but formulated withinIsabelle's meta logic: <strong>Isabelle/Pure</strong>. There arequite a lot of syntactic and deductive tools available in genericIsabelle. Thus defining new logics or extending existing onesbasically works as follows:<ol><li> declare concrete syntax (via mixfix grammar and syntax macros),<li> declare abstract syntax (as higher-order constants),<li> declare inference rules (as meta-logical propositions),<li> instantiate generic automatic proof tools (simplifier, classicaltableau prover etc.),<li> manually code special proof procedures (via tacticals orhand-written ML).</ol>The first three steps above are fully declarative and involve no MLprogramming at all. Thus one already gets a decent deductiveenvironment based on primitive inferences (by employing the built-inmechanisms of Isabelle/Pure, in particular higher-order unificationand resolution).For sizable applications some degree of automated reasoning isessential. Instantiating existing tools like the classical tableauprover involves only minimal ML-based setup. One may also writearbitrary proof procedures or even theory extension packages in ML,without breaching system soundness (Isabelle follows the well-known<em>LCF system approach</em> to achieve a secure system).<h2>Mailing list</h2>Use the mailing list <a href="mailto:isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a> todiscuss problems and results. (Why not <A HREF="mailto:lcp@@cl.cam.ac.uk">subscribe</A>?)</body></html>