Technical Report 2021-001

Towards Correctly Checking for Cycles in Overloaded Definitions

Arve Gengelbach and Johannes Åman Pohjola

March 2021

Abstract:
Safe extension of a logic with definitional axioms need acyclic definitions, because cycles in definitions possibly entail contradiction. In this report we give a mechanised exact characterisation of acyclic overloading definitions. Our results support the soundness argument of the cyclicity checker of the Isabelle/HOL theorem prover, and serve as the theoretical foundation for future verification of such a cyclicity checker.

Available as PDF (421 kB, no cover)

Download BibTeX entry.