Correctness of Isabelle's Cyclicity Checker: Implementability of Overloading in Proof Assistants

Abstract

Overloaded constant definitions are an important feature of the proof assistant Isabelle because they allow us to provide Haskell-like type classes to our users. There has been an ongoing question as to under which conditions we can practically guarantee that overloading is a safe theory extension, i.e., preserves consistency or is conservative. The natural condition is that a rewriting system generated by overloaded definitions must always terminate. The current system imposes restrictions on accepted overloaded definitions and decides the termination by an algorithm that is part of the trusted code base of Isabelle. Therefore we aim to prove its correctness.