Isabelle (proof assistant)

Isabelle
	Isabelle/jEdit running on macOS
Original author(s)	Lawrence Paulson
Developer(s)	University of Cambridge and Technical University of Munich et al.
Initial release	1986
Stable release	Isabelle2024 / May 2024
Written in	Standard ML and Scala
Operating system	Linux, Windows, macOS
Type	Mathematics
License	BSD license
Website	isabelle.in.tum.de

The Isabelle^[a] automated theorem prover is a higher-order logic (HOL) theorem prover, written in Standard ML and Scala. As an LCF-style theorem prover, it is based on a small logical core (kernel) to increase the trustworthiness of proofs without requiring — yet supporting — explicit proof objects.

Isabelle is available inside a flexible system framework allowing for logically safe extensions, which comprise both theories as well as implementations for code-generation, documentation, and specific support for a variety of formal methods. It can be seen as an IDE for formal methods. In recent years, a substantial number of theories and system extensions have been collected in the Isabelle Archive of Formal Proofs (Isabelle AFP)^[2]

Isabelle was named by Lawrence Paulson after Gérard Huet's daughter.^[3]

The Isabelle theorem prover is free software, released under the revised BSD license.

^ Paulson, L. C. (1986). "Natural deduction as higher-order resolution". The Journal of Logic Programming. 3 (3): 237–258. arXiv:cs/9301104. doi:10.1016/0743-1066(86)90015-4. S2CID 27085090.
^ Eberl, Manuel; Klein, Gerwin; Nipkow, Tobias; Paulson, Larry; Thiemann, René. "Archive of Formal Proofs". Retrieved 1 May 2021.
^ Gordon, Mike (1994-11-16). "1.2 History". Isabelle and HOL. Cambridge AR Research (The Automated Reasoning Group). Archived from the original on 2017-03-05. Retrieved 2016-04-28.

Cite error: There are <ref group=lower-alpha> tags or {{efn}} templates on this page, but the references will not show without a {{reflist|group=lower-alpha}} template or {{notelist}} template (see the help page).

[1] Paulson, L. C. (1986). "Natural deduction as higher-order resolution". The Journal of Logic Programming. 3 (3): 237–258. arXiv:cs/9301104. doi:10.1016/0743-1066(86)90015-4. S2CID 27085090.

[3] Eberl, Manuel; Klein, Gerwin; Nipkow, Tobias; Paulson, Larry; Thiemann, René. "Archive of Formal Proofs". Retrieved 1 May 2021.

[4] Gordon, Mike (1994-11-16). "1.2 History". Isabelle and HOL. Cambridge AR Research (The Automated Reasoning Group). Archived from the original on 2017-03-05. Retrieved 2016-04-28.

[1]

[a]

[2]

[3]