Senior software architect
R&D team lead

Tweag I/O

email: firstname_at_surname.net

Cellphone :

Here are some software I contribute to:

• Coq the most successful implementation of a dependent type theory. Serves both as a programming language and a proof assistant. Coq is a central object in my research.
• Melt an Ocaml library and preprocessor to generate Latex documents. It saved me countless hours and immense frustration. It is still a little too much tailored to the needs of the few contributors, and development is going slowly. But you may still consider using it.

I have more experimental things going on:

• My github address may be a good place to get fresh news.