4 papers · 1 filter
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…
Kuroda's Translation for Higher-Order Logic
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 Ri…
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…
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…