Interested in studying in my group? Please see the page on Ph.D. at INRIA and the F.A.Q..

Current Ph.D. students

Nathanaëlle Courant, since 2019. Topic: efficient, formally-verified convertibility checkers for Coq and related proof assistants.

Past Ph.D. students

Basile Clément, 2019-2022. Topic: Translation validation of tensor compilers.

Jacques-Henri Jourdan, 2012-2016. Topic: Verasco: a formally-verified C static analyzer. Jacques-Henri is currently a CNRS research scientist at Laboratoire Méthodes Formelles of Université Paris-Sud.

Tahina Ramananandro, 2007-2011. Topic: Mechanized formal semantics and verified compilation for C++ objects. Tahina is currently a senior research software development engineer at Microsoft Research, Redmond.

Jean-Baptiste Tristan, 2006-2009. Topic: Formal verification of translation validation. Jean-Baptiste is currently principal scientist at AWS and associate professor at Boston College.

Zaynah Dargaye, 2005-2009. Topic: Certified compilation of functional languages. Zaynah is currently with the Nomadic Labs company in Paris.

Tom Hirschowitz, 2000-2003. Topic: Mixin modules for call-by-value languages. Tom is currently a CNRS senior research scientist, working at the LAMA laboratory of Savoie Mont Blanc University.

Benjamin Grégoire, 1999-2003, co-advised with Benjamin Werner. Topic: Compilation of Coq proof terms. Benjamin is currently an INRIA research scientist, working at the Marelle team of INRIA Sophia-Antipolis.

François Pessaux, 1997-1999. Topic: Type-based static analysis of uncaught exceptions. François is currently assistant professor at ENSTA ParisTech.

Past Master's interns

All of the above, plus:

Ambroise Lafont, 2016. Topic: the Coqonut verified compiler for the Coq specification language. Ambroise is currently a post-doctoral fellow at Cambridge University.

Boris Yakobowski, 2004. Topic: A semantic study of SSA form. Boris is now R&D engineer at Adacore, Paris.

François Pottier, 1994. Topic: An SML-style module system for Caml Light. François is currently a senior research scientist at INRIA Paris, and head of the Cambium research team.