Ondřej Kunčar
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.
Thanks to our work we discovered not only completeness shortcomings but also a correctness issue---we could prove False. In our paper we present a modified version of the algorithm together with a proof of completeness and correctness of it.
Although our work deals with Isabelle, our paper provides a more general result: how to practically implement overloading in proof assistants.
- URL http://www21.in.tum.de/~kuncar/documents/issues.Google Scholar
- A. Grabowski, A. Kornilowicz, and A. Naumowicz. Mizar in a Nut- shell. J. Formalized Reasoning, 3(2):153--245, 2010.Google Scholar
- F. Haftmann and M. Wenzel. Constructive Type Classes in Isabelle. In T. Altenkirch and C. McBride, editors, TYPES, volume 4502 of Lecture Notes in Computer Science, pages 160--174. Springer, 2006. Google ScholarDigital Library
- T. Nipkow and Z. Qian. Reduction and Unification in Lambda Calculi with Subtypes. In D. Kapur, editor, CADE, volume 607 of Lecture Notes in Computer Science, pages 66--78. Springer, 1992. Google ScholarDigital Library
- S. Obua. Checking Conservativity of Overloaded Definitions in Higher- Order Logic. In F. Pfenning, editor, RTA, volume 4098 of Lecture Notes in Computer Science, pages 212--226. Springer, 2006. Google ScholarDigital Library
- M. Sozeau and N. Oury. First-Class Type Classes. In O. A. Mohamed, C. M. Muñoz, and S. Tahar, editors, Theorem Proving in Higher Order Logics, volume 5170 of Lecture Notes in Computer Science, pages 278--293. Springer, 2008. Google ScholarDigital Library
- M. Wenzel. Type Classes and Overloading in Higher-Order Logic. In E. L. Gunter and A. P. Felty, editors, Theorem Proving in Higher Order Logics, volume 1275 of Lecture Notes in Computer Science, pages 307--322. Springer, 1997. Google ScholarCross Ref
Index Terms
- Correctness of Isabelle's Cyclicity Checker: Implementability of Overloading in Proof Assistants
Recommendations
A Formalization and Proof Checker for Isabelle’s Metalogic
AbstractIsabelle is a generic theorem prover with a fragment of higher-order logic as a metalogic for defining object logics. Isabelle also provides proof terms. We formalize this metalogic and the language of proof terms in Isabelle/HOL, define an ...
Bounded Model Generation for Isabelle/HOL
A translation from higher-order logic (on top of the simply typed λ-calculus) to propositional logic is presented, such that the resulting propositional formula is satisfiable iff the HOL formula has a model of a given finite size. A standard SAT solver ...
Self-Formalisation of Higher-Order Logic
We present a mechanised semantics for higher-order logic (HOL), and a proof of soundness for the inference system, including the rules for making definitions, implemented by the kernel of the HOL Light theorem prover. Our work extends Harrison's ...
Comments