Benjamin Werner's page

Benjamin Werner's home page

I am a researcher working for INRIA; as such:

I am (co-)leading the LogiCal team, located at the LIX laboratory of the Ecole Polytechnique (directions).

I am also member of the mathematical components team of the INRIA/Microsoft Research joint centre (directions).


version française

Frege's Begriffsschrift

Research

My research interests lie in the formalization of mathematical reasoning and its mechanical verification through proof systems, especially Coq. Currently, I am particularly interested by proofs involving computations and evolutions of type theory making this easier.

Publications and papers

A video lecture (in french) about formal proofs which involve computations

Some other stuff for a (slightly) wider audience.

A short CV.

Le Galibier

Teaching

Teaching material

Cours 2-7-1, MPRI 2010

PhD students

Bruno Barras (defended 1999)
David Delahaye (defended 2001)
Benjamin Grégoire (co-advised with Xavier Leroy; defended 2003)
Roland Zumkeller (since 2004)
Arnaud Spiwack (co-advised with Thierry Coquand since 2006)

How to reach me

This page: http://benjamin.werner.name

email:

Main address:

LIX, Ecole Polytechnique, F-91128 PALAISEAU cedex, France
phone: + 33 1 69 33 41 41 (polytechnique new number)
going to Polytechnique
going to the INRIA/MSR joint centre