14 citations · 58 across the 10 of their papers we have counts for
6 papers · 1 filter
Arithmetic as a theory modulo
Gilles Dowek, Benjamin Werner
We present constructive arithmetic in Deduction modulo with rewrite rules only.
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…
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…
Formal Proofs for Nonlinear Optimization
Victor Magron, Xavier Allamigeon, Stéphane Gaubert +1
We present a formally verified global optimization framework. Given a semialgebraic or transcendental function and a compact semialgebraic domain , we use the nonlinear maxp…
Proof-irrelevant model of CC with predicative induction and judgmental equality
Gyesik Lee, Benjamin Werner
We present a set-theoretic, proof-irrelevant model for Calculus of Constructions (CC) with predicative induction and judgmental equality in Zermelo-Fraenkel set theory with an axio…
On the strength of proof-irrelevant type theories
Benjamin Werner
We present a type theory with some proof-irrelevance built into the conversion rule. We argue that this feature is useful when type theory is used as the logical formalism underlyi…