Benjamin Werner's page

Benjamin Werner's home page

I am a researcher working for INRIA; as such:

I am leading the TypiCal (formely 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

My Calendar

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 vitae in english and in french (pdf).

Le Galibier

Teaching

Teaching material

PhD students

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

How to reach me

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

New: My calendar (mon agenda)

email:

Main address:

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

I also like taking photographs; here are some I shot.