Papers about Isabelle
Isabelle has become one of the world's most popular proof assistants. It supports a variety of formalisms, including set theory, but the most popular by far is its implementation of higher order logic. This instance of Isabelle is called Isabelle/HOL.
[Note: Look elsewhere for Isabelle documentation]
- Basic Concepts
- On the classical reasoner
- Of historical interest
- L. C. Paulson.
The foundation of a generic theorem prover. J. Automated Reasoning 5 (1989), 363–397. Publisher's version - L. C. Paulson.
Isabelle: the next 700 theorem provers. In: P. Odifreddi (editor), Logic and Computer Science (Academic Press, 1990), 361–386. - L. C. Paulson.
Tool support for logics of programs. In: M. Broy (editor), Mathematical Methods in Program Development (Summer School Marktoberdorf 1996), Springer-Verlag, 461–498. Also Report 406, Computer Lab (1996). Slides available - Strategic principles in the design of Isabelle.
CADE-15 Workshop on Strategies in Automated Deduction, Lindau, Germany (1998), 11–17.
Slides available
- L. C. Paulson,
Generic automatic proof tools. In: Robert Veroff (editor), Automated Reasoning and its Applications: Essays in Honor of Larry Wos (MIT Press, 1997), 23–47. - L. C. Paulson,
A generic tableau prover and its integration with Isabelle.
J. Universal Computer Science 5 3 (1999), 73–87.
See also papers on linking Isabelle with automatic provers.
- L. C. Paulson.
Natural deduction as higher-order resolution. J. Logic Programming 3 (1986), 237–258. - L. C. Paulson.
Isabelle: the next seven hundred theorem provers (system abstract). In: E. Lusk and R. Overbeek (editors), 9th International Conf. on Automated Deduction (Springer LNCS 310, 1988), 772–773. - L. C. Paulson.
A formulation of the simple theory of types (for Isabelle). In: P. Martin-Löf &G. Mints (editors), COLOG-88: International Conf. in Computer Logic.Tallinn, Estonia (1988). Published as Springer LNCS 417, 1990), 246–274. - L. C. Paulson.
A preliminary user's manual for Isabelle. Technical Report 133, Computer Lab (1988). - Tobias Nipkow and L C Paulson,
Isabelle tutorial and user's manual. Technical Report 189, Computer Lab (1990). - L. C. Paulson.
Isabelle’s Object-Logics. Technical Report 286, Computer Lab (1993).
(This version is dated November 1997.)
- L. C. Paulson,
Introduction to Isabelle. Technical Report, Computer Lab (last revised 2003).
Research funded by the EPSRC grant numbers GR/E0355.7, GR/H40570, GR/K57381, GR/S57198/01 and many others.