Thomas Traversié

Thomas Traversié, Florian Rabe

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.

Thomas Traversié

Kuroda's translation embeds first-order classical logic into intuitionistic logic, such that a formula and its translation are equivalent in classical logic. Recently, Brown and Rizkallah extended this translation to higher-order logic. However, they showed that the translation fails in the presence of functional extensionality, and they did not prove the classical equivalence between a formula and its translation. In this paper, we emphasize different conditions under which Kuroda's translation works in the presence of functional extensionality, including the double-negation shift. We show that the classical equivalence between a formula and its translation does not necessarily hold in higher-order logic. However, it is sufficient to assume both functional extensionality and propositional extensionality.