Papers about IsabelleIsabelle logo

Isabelle has become one of the world's most popular proof assistants. It supports a variety of formalisms, including ZF 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

EPSRC logo
Research funded by the EPSRC grant numbers GR/E0355.7, GR/H40570, GR/K57381, GR/S57198/01 and many others.

Last revised: 8 July, 2014

Lawrence C. PaulsonComputer LaboratoryUniversity of Cambridge