arXiv subjects

Thomas Traversié

Publications and source records attributed to Thomas Traversié.

5 recordsLinked to original sources

arXiv2026

Formalizing Representation Theorems for a Logical Framework with Rewriting

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.

cs.LO↗

arXiv2026

Kuroda's Translation for Higher-Order Logic

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.

cs.LO↗

arXiv2024

Kuroda's Translation for the $λΠ$-Calculus Modulo Theory and Dedukti

Kuroda's translation embeds classical first-order logic into intuitionistic logic, through the insertion of double negations. Recently, Brown and Rizkallah extended this translation to higher-order logic. In this paper, we adapt it for theories encoded in higher-order logic in the lambdaPi-calculus modulo theory, a logical framework that extends lambda-calculus with dependent types and user-defined rewrite rules. We develop a tool that implements Kuroda's translation for proofs written in Dedukti, a proof language based on the lambdaPi-calculus modulo theory.

cs.LO↗

arXiv2024

Proofs for Free in the $λΠ$-Calculus Modulo Theory

Parametricity allows the transfer of proofs between different implementations of the same data structure. The lambdaPi-calculus modulo theory is an extension of the lambda-calculus with dependent types and user-defined rewrite rules. It is a logical framework, used to exchange proofs between different proof systems. We define an interpretation of theories of the lambdaPi-calculus modulo theory, inspired by parametricity. Such an interpretation allows to transfer proofs for free between theories that feature the notions of proposition and proof, when the source theory can be embedded into the target theory.

cs.LO↗

arXiv2024

From Rewrite Rules to Axioms in the $λ$$Π$-Calculus Modulo Theory

The $λ$$Π$-calculus modulo theory is an extension of simply typed $λ$-calculus with dependent types and user-defined rewrite rules. We show that it is possible to replace the rewrite rules of a theory of the $λ$$Π$-calculus modulo theory by equational axioms, when this theory features the notions of proposition and proof, while maintaining the same expressiveness. To do so, we introduce in the target theory a heterogeneous equality, and we build a translation that replaces each use of the conversion rule by the insertion of a transport. At the end, the theory with rewrite rules is a conservative extension of the theory with axioms.

cs.LO↗