14 citations · 58 across the 10 of their papers we have counts for
10 papers
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…
A drag-and-drop proof tactic
Pablo Donato, Pierre-Yves Strub, Benjamin Werner
We explore the features of a user interface where formal proofs can be built through gestural actions. In particular, we show how proof construction steps can be associated to drag…
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…
Certification of Real Inequalities -- Templates and Sums of Squares
Xavier Allamigeon, Stéphane Gaubert, Victor Magron +1
We consider the problem of certifying lower bounds for real-valued multivariate transcendental functions. The functions we are dealing with are nonlinear and involve semialgebraic…
Certification of inequalities involving transcendental functions: combining SDP and max-plus approximation
Xavier Allamigeon, Stéphane Gaubert, Victor Magron +1
We consider the problem of certifying an inequality of the form , , where is a multivariate transcendental function, and is a compact semialgebr…
Certification of Bounds of Non-linear Functions: the Templates Method
Xavier Allamigeon, Stéphane Gaubert, Victor Magron +1
The aim of this work is to certify lower bounds for real-valued multivariate functions, defined by semialgebraic or transcendental expressions. The certificate must be, eventually,…
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…