3 papers
cs.LO2025
Formalizing Representation Theorems for a Logical Framework with Rewriting
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 log…
cs.LO2024
Proofs for Free in the -Calculus Modulo Theory
Thomas Traversié
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…
cs.LO2024
Kuroda's Translation for the -Calculus Modulo Theory and Dedukti
Thomas Traversié
Kuroda's translation embeds classical first-order logic into intuitionistic logic, through the insertion of double negations. Recently, Brown and Rizkallah extended this translatio…