A consistent foundation for Isabelle/HOL

The interactive theorem prover Isabelle/HOL is based on well understood Higher-Order Logic (HOL), which is widely believed to be consistent (and provably consistent in set theory by a standard semantic argument). However, Isabelle/HOL brings its own personal touch to HOL: overloaded constant definitions, used to achieve Haskell-like type classes in the user space. These features are a delight for the users, but unfortunately are not easy to get right as an extension of HOL—they have a history of inconsistent behavior. It has been an open question under which criteria overloaded constant definitions and type definitions can be combined together while still guaranteeing consistency. This paper presents a solution to this problem: non-overlapping definitions and termination of the definition-dependency relation (tracked not only through constants but also through types) ensures relative consistency of Isabelle/HOL.

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-22102-1_16

Cite this paper as:
Kunčar O., Popescu A. (2015) A Consistent Foundation for Isabelle/HOL. In: Urban C., Zhang X. (eds) Interactive Theorem Proving. ITP 2015. Lecture Notes in Computer Science, vol 9236. Springer, Cham