I'm involved in the JSCert project, which aims at certifying analyses for JavaScript. The formalization of the language is available on github. We also have developed JSExplain, a visual debugger for the JavaScript Specification.

Kévin le Bon has developed MLExplain, a visual debugger for an OCaml interpreter, based on JSExplain. You can run it here and see the code here.

Simon Boulier, Martín Escarrà, Petar Maksimović, and I are proving results from this paper on HOcore in Coq. The current development can be browsed here.

Previously, I worked on the Kell Calculus and more generally on programming languages for component-based systems. I also developed static analyses for distributed systems. I collaborated with Davide Sangiorgi at Università di Bologna working on the expressiveness of process calculi, and with Nabil Layaïda and Pierre Genevès of the WAM team at INRIA on static analyses for XPath.

I was part of the Harmony Project in collaboration with Benjamin C. Pierce at the University of Pennsylvania.

I am a member of the steering committee (comité de pilotage) of the Journées Francophones des Langages Applicatifs (JFLA). I was president of the JFLA in 2009 and vice-president in 2008.

I participated in the program committees of the following conferences and workshops.