Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Benjamin Werner

Benjamin Werner

Photo by Hugo Herbelin

Researcher INRIA, Rocquencourt, projet Coq.

This page is hopelessly out of daye and is to be moved soon. However, here is a draft of the long version of a paper with Gilles Dowek on Arithmetic as a theory modulo.

La page du cours de DEA "Calcul des Constructions Inductives".
Ma page à l'École Polytechnique.

Research Interests:

Type Theory; Formal Mathematics; Constructive Proofs; Applications to Software Validation.
The Coq proof assistant.

New Stuff

Coq in Coq (submitted). Joint work with Bruno Barras. Click for dvi version or postscript.
The Encoding of Zermolo-Fraenkel Set Theory in Coq (TACS'97) (Coq text file - 38k).
A Generic Normalization Proof for Pure Type Systems (TYPES'96). Joint Work with Paul-André Melliès. Click for postscript version and dvi version.
On the Definition of the Eta-long Normal Form (submitted). Joint work with Gilles Dowek and Gérard Huet. Click for dvi version or postscript version.

More information:

Finger info.
Some publications.
Teaching activities (with course notes).
Some pointers about formal mathematics.
Some non-professional pointers.
Some postcards.

Benjamin.Werner@inria.fr