Current Ph.D. students
Jacques-Henri Jourdan, since 2012. Topic: formal verification of static analyzers based on abstract interpretation.
Past Ph.D. students
Mechanized formal semantics and verified compilation for C++ objects.
Tahina is currently a senior engineer at Reservoir Labs, NY.
Tristan, 2006-2009. Topic:
Formal verification of translation validation. Jean-Baptiste is currently a research scientist at Oracle Labs.
2005-2009. Topic: Certified compilation of functional languages. Zaynah is currently a scientist at CEA, LIST laboratory.
modules for call-by-value languages. Tom is currently
a CNRS research scientist, working at the LAMA laboratory of
Université de Savoie.
Grégoire, 1999-2003, co-advised with
of Coq proof terms. Benjamin is currently an INRIA research scientist,
working at the Marelle team of INRIA Sophia-Antipolis.
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:
2004. Topic: A
semantic study of SSA form. Boris is now a scientist at CEA, LIST laboratory.
1994. Topic: An
SML-style module system for Caml Light. François is currently
a senior research scientist at INRIA Paris-Rocquencourt, Gallium team.