34 citations
- Laboratoire de Mesure du Carbone 14FR9 papers
- Institut national de recherche en sciences et technologies du numériqueFR5 papers
- Université Paris-SaclayFR5 papers
- Centre National de la Recherche ScientifiqueFR4 papers
- École Normale Supérieure Paris-SaclayFR4 papers
- École PolytechniqueFR4 papers
- Mathématiques et Informatique pour la Complexité et les Systèmes3 papers
- CentraleSupélecFR2 papers
- Centre Inria de SaclayFR2 papers
- Laboratoire d'Informatique de l'École PolytechniqueFR2 papers
- Aix-Marseille UniversitéFR1 paper
- Atos (France)FR1 paper
Showing 2024Show all
3 papers · 1 filter
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…
cs.LO2024
From Rewrite Rules to Axioms in the -Calculus Modulo Theory
Valentin Blot, Gilles Dowek, Thomas Traversié +1
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 rewri…