The Isabelle Framework

10 years 2 months ago
The Isabelle Framework
g to the well-known “LCF approach” of secure inferences as abstract datatype constructors in ML [16]; explicit proof terms are also available [8]. Isabelle/Isar provides sophisticated extra-logical infrastructure supporting structured proofs and specifications, including concepts for modular theory development. Isabelle/HOL is a large application within the generic framework, with plenty of logic-specific add-on tools and a large theory library. Other notable object-logics are Isabelle/ZF (Zermelo-Fraenkel set-theory, see [34, 36]) and Isabelle/HOLCF [26] (Scott’s domain theory within HOL). Users can build further formal-methods tools on top, e.g. see [53]. Beginners are advised to start working with Isabelle/HOL; see the tutorial volume [30], and the companion tutorial [28] covering structured proofs. A general impression of Isabelle/HOL and ZF compared to other systems like Coq, PVS, Mizar etc. is given in [52]. The Proof General Emacs interface [3] is still the de-facto stan...
Makarius Wenzel, Lawrence C. Paulson, Tobias Nipko
Added 01 Jun 2010
Updated 01 Jun 2010
Type Conference
Year 2008
Authors Makarius Wenzel, Lawrence C. Paulson, Tobias Nipkow
Comments (0)