Formalizing Representation Theorems for a Logical Framework with Rewriting
This work addresses the problem of simplifying formal verification for researchers in formal logic and theorem proving, though it is incremental as it builds on existing frameworks.
The paper tackles the challenge of formalizing and verifying representation theorems in logical frameworks by extending the lambdaPi-calculus modulo rewriting with theory morphisms and logical relations, resulting in easier and more elegant formalizations of translations such as sort-erasure from sorted to unsorted languages.
Representation theorems for formal systems often take the form of an inductive translation that satisfies certain invariants, which are proved inductively. Theory morphisms and logical relations are common patterns of such inductive constructions. They allow representing the translation and the proofs of the invariants as a set of translation rules, corresponding to the cases of the inductions. Importantly, establishing the invariants is reduced to checking a finite set of, typically decidable, statements. Therefore, in a framework supporting theory morphisms and logical relations, translations that fit one of these patterns become much easier to formalize and to verify. The lambdaPi-calculus modulo rewriting is a logical framework designed for representing and translating between formal systems that has previously not systematically supported such patterns. In this paper, we extend it with theory morphisms and logical relations. We apply these to define and verify invariants for a number of translations between formal systems. In doing so, we identify some best practices that enable us to obtain elegant novel formalizations of some challenging translations, in particular sort-erasure translations from sorted to unsorted languages.