Gilles Dowek

activity

20052023

most citedLineal: A linear-algebraic Lambda-calculus

34 citations · 144 across the 66 of their papers we have counts for

collaborators

Showing 2015 · cs.LOShow all

3 papers · 2 filters

cs.LO2015

Deduction modulo theory

Gilles Dowek

This paper is a survey on Deduction modulo theory

cs.LO2015

Models and termination of proof reduction in the $λ$ $Π$ -calculus modulo theory

Gilles Dowek

We define a notion of model for the $λ$ $Π$ -calculus modulo theory and prove a soundness theorem. We then define a notion of super-consistency and prove that proof reduction termina…

cs.LO2015

Proof Normalisation in a Logic Identifying Isomorphic Propositions

Alejandro Díaz-Caro, Gilles Dowek

We define a fragment of propositional logic where isomorphic propositions, such as $A \land B$ and $B \land A$ , or $A \Rightarrow (B \land C)$ and $(A\Rightarrow B)\land(A\Rightarrow C…

Deduction modulo theory

Models and termination of proof reduction in the λΠ-calculus modulo theory

Proof Normalisation in a Logic Identifying Isomorphic Propositions

Models and termination of proof reduction in the $λ$ $Π$ -calculus modulo theory