My research globally centres around the syntactic unity between proofs and programs, with applications to:

My master is from 1988, but in the 1989-1992 period, it happens that I was more concerned with my newly-born now-adult daughter than with research.

I worked from 1993 on the computational content of sequent calculus and on its relation to the theory of programming languages (ch. 2 of PhD thesis, CSL94), contributing at the same time to a better understanding of the proof-as-program correspondence for classical logic (ch. 3 of PhD thesis, ICFP00 with Pierre-Louis Curien, ch. 1 to 3 of Habilitation).

I worked from 1994 on the syntactic view at game semantics (ch. 5 and 6 of PhD thesis, LICS96 with Vincent Danos and Laurent Régnier, TLCA97, FLOPS98 with Pierre-Louis Curien), which is closely connected to sequent calculus and abstract machines. After some time, I prefered to work directly with syntax than via a "semantical" game-theoretic abstraction of it. I liked my old note decomposing AJM games into HO games and P-digitalisation, but I felt this was not at all an approach the at-this-time dominant British school was interested in.

In the 1996-1999 period, I devoted relatively quite a lot of time to teaching, system engineering, and understanding Coq's insides, fascinated by what Gérard Huet and Thierry Coquand created, altogether with the team they built. It was not a period for intense foundational research and the refusal at LICS of the ad hoc arity-based abstract machine for System F I was so proud about hurt me a lot. The paper is still not published (the referees were however right that the presentation was obscured by overly complex notations).

With Zena Ariola, I started to apply the proof-as-program correspondence for classical logic to a better understanding of control operators in programming languages (ICALP03/HOSC05, JFP07, TLCA09 with Stéphane Zimmermann, and a yet unpublished kind of survey with Alexis Saurin), what eventually also targeted call-by-need evaluation (TLCA11, FLOPS12).

From 2003 to 2008, I approached Felleisen and Danvy-Filinski's notion of delimited control in programming languages using Parigot's tools to the proof-as-program correspondence for classical logic. This resulted, first with Zena Ariola and Amr Sabry, then with Silvia Ghilezan, in a fine-grained account of delimited control (ICFP04/HOSC07, ch. 4 of Habilitation, POPL08).

I've never been able to figure out whether it was already clear from 1993 for Catarina Coquand, Thierry Coquand, Ulrich Berger or others that reducibility proofs had the same computational structure as normalisation-by-evaluation proofs, so, around 2008, I wrote a note on it. I still don't know if what it says was known or not.

Inspired by the use of delimited control by Olivier Danvy in Typed-Directed Partial Evaluation (TDPE) and by the relation between TDPE and Normalisation-by-Evaluation (NbE), I started to work with Danko Ilik on the computational content of completeness proofs in relation with NbE and delimited control. This has turned to be a very fruitful field of investigation.

First, it moved to a precise analysis of the computational content of Gödel's completeness therorem proofs (in progress) and to the analysis of Krikpe semantics in a classical setting (WOLLIC09, APAL10).

More importantly, it moved to the study of the proof-as-program correspondence in the presence of other side effects than classical logic, especially delimiters (LICS10), sharing (with application to computing with dependent choice, LICS12) or memory assignment. In the latter case, this directly connects to forcing as shown by Jean-Louis Krivine in the context of realisability.

Recently, I started to take a computational view at reverse mathematics, with Gyesik Lee, Keiko Nakata and Ludovic Patey (the constructive content of the big five, an effective type-theoretic presentation of PRA).

These days, as an entertainment related to the homotopical foundations of type theory, I'm also working on the formal representation of semi-simplicial types (MSCS14, and more is to come).

All over the period from 1988 to now, Coq was a faithful companion to the loneliness of my mind. I contributed to its implementation, especially intensively from 1996 to 2008, as well as to the coordination of its development. From time to time, I also contributed to the foundations of type theory (JFP94 on a proposal of Thierry Coquand, TLCA05, TYPES08, as well as LICS10 and JFP11 with Vincent Siles).