Isabelle (proof assistant)
| Isabelle | |
|---|---|
Isabelle–jEdit running on macOS | |
| Original author(s) | Lawrence Paulson |
| Developer(s) | University of Cambridge Technical University of Munich, et al. |
| Initial release | 1986 |
| Stable release | Isabelle2025
/ March 2025 |
| Written in | Standard ML, Scala |
| Operating system | Linux, Windows, macOS |
| Type | Mathematics |
| License | BSD |
| Website | isabelle |
The Isabelle automated theorem prover is a higher-order logic (HOL) theorem prover, written in Standard ML and Scala. As a Logic for Computable Functions (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 and implementations for code-generating, documenting, and specific support for a variety of formal methods. It can be seen as an integrated development environment (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).
Isabelle was named by Lawrence Paulson after Gérard Huet's daughter.
The Isabelle theorem prover is free software, released under the revised BSD license.