Paper Info
Title
The Isabelle Framework
Abstract
Isabelle, which is available from http://isabelle.in.tum.de, is a generic framework for interactive theorem proving. The Isabelle/Pure meta-logic allows the formalization of the syntax and inference rules of a broad range of object-logics fol- lowing the general idea of natural deduction (32, 33). The logical core is implemented according 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 pro- vides sophisticated extra-logical infrastructure supporting structured proofs and speci- fications, 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 standard for interaction with Isabelle. The Isabelle document preparation system enables one to generate high- quality PDF-LAT E X documents from the original theory sources, with full checking of the formal content. The Archive of Formal Proofs http://afp.sf.net collects proof libraries, ex- amples, and larger scientific developments, mechanically checked with Isabelle. AFP is organized like a journal everybody can contribute to. Submitting formal theories there helps to maintain applications in the longer term, synchronized with the ongoing devel- opment of Isabelle itself.
Year
DOI
Venue
2008
10.1007/978-3-540-71067-7_7
Theorem Proving in Higher Order Logics
Keywords
Field
DocType
zermelo-fraenkel set-theory,domain theory,abstract datatype constructor,notable object-logics,modular theory development,isabelle framework,generic framework,isarprovides sophisticated extra-logical infrastructure,large theory library,lcf approach,large application,natural deduction,inference rule,formal method,interactive theorem proving,set theory
HOL,Programming language,Prime number theorem,Natural deduction,Computer science,Domain theory,Algorithm,Theoretical computer science,Mathematical proof,Syntax,Rule of inference,Proof assistant
Conference
Volume
ISSN
Citations 
5170
0302-9743
34
PageRank 
References 
Authors
1.32
46
3
Name
Order
Citations
PageRank
Makarius Wenzel127224.39
Lawrence C. Paulson22929265.05
Tobias Nipkow33056232.28