A Verified Cyclicity Checker: For Theories with Overloaded Constants

Autor:	Gengelbach, Arve, Åman Pohjola, Johannes
Jazyk:	angličtina
Rok vydání:	2022
Předmět:	Theory of computation → Graph algorithms analysis Software and its engineering → Correctness definitions non-termination Theory of computation → Program verification Theory of computation → Higher order logic ad-hoc overloading Isabelle/HOL cyclicity
DOI:	10.4230/lipics.itp.2022.15
Popis:	Non-terminating (dependencies of) definitions can lead to logical contradictions, for example when defining a boolean constant as its own negation. Some proof assistants thus detect and disallow non-terminating definitions. Termination is generally undecidable when constants may have different definitions at different type instances, which is called (ad-hoc) overloading. The Isabelle/HOL proof assistant supports overloading of constant definitions, but relies on an unclear foundation for this critical termination check. With this paper we aim to close this gap: we present a mechanised proof that, for restricted overloading, non-terminating definitions are of a detectable cyclic shape, and we describe a mechanised algorithm with its correctness proof. In addition we demonstrate this cyclicity checker on parts of the Isabelle/HOL main library. Furthermore, we introduce the first-ever formally verified kernel of a proof assistant for higher-order logic with overloaded definitions. All our results are formalised in the HOL4 theorem prover. LIPIcs, Vol. 237, 13th International Conference on Interactive Theorem Proving (ITP 2022), pages 15:1-15:18
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::1726c08a47a87c1140fc2915702b143c Zobrazit plný text záznamu