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...

• Type: Conference
• Year: 2008
• Where: TPHOL
• Authors: Makarius Wenzel, Lawrence C. Paulson, Tobias Nipkow
• Keywords: Abstract Datatype Constructors, Artificial Intelligence, Explicit Proof Terms, Structured Proofs, TPHOL 2008