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
18 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…
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…
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…
A Complete Proof Synthesis Method for the Cube of Type Systems
Gilles Dowek
We present a complete proof synthesis method for the eight type systems of Barendregt's cube extended with -conversion. Because these systems verify the proofs-as-objects paradi…
A constructive proof of Skolem theorem for constructive logic
Gilles Dowek, Benjamin Werner
If the sequent (Gamma entails forall x exists y A) is provable in first order constructive natural deduction, then the theory (Gamma, forall x (f (x)/y)A), where f is a new functio…