Lambda the Ultimate

PhD in 1991 on programming language environments (worked on precursors
to Eclipse, in a way),
Then developed a precursor to Proof General, but so difficult to
install it did not get as wide a user basis,
Then wrote the Coq'Art with Pierre Castéran (published in 2004),
Experimented in proofs of algorithms in a variety of domains:
computer arithmetics, Programming language semantics, computational
geometry, exact real arithmetic, algebra, streams...

Current subjects of focus (fall 2008):
1 formal study (ie. modeling and proving) for:
- exact real number arithmetics,
- real arithmetic decision procedures,
- geometry,
- computation and proofs with infinite streams.

2/ making the concepts and methods of theorem proving more accessible
- tutorials,
- exercises,