14 citations · 58 across the 10 of their papers we have counts for
Showing 2023 · cs.LOShow all
3 papers · 2 filters
cs.LO2023
Arithmetic as a theory modulo
Gilles Dowek, Benjamin Werner
We present constructive arithmetic in Deduction modulo with rewrite rules only.
cs.LO2023
On the Definition of the Eta-long Normal Form in Type Systems of the Cube
Gilles Dowek, Gérard Huet, Benjamin Werner
The smallest transitive relation < on well-typed normal terms such that if t is a strict subterm of u then t < u and if T is the normal form of the type of t and the term t is not…
cs.LO2023★ 1 cited
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…