I work at Inria and LIX, where I do research in Mathematical Logic and Theoretical Computer Science.

The main aim of my work has been to modernize proof theory and the foundations of constructive mathematics using distilled computing abstractions from the theory of programming languages such as delimited control operators, partial evaluators and type isomorphisms. One can see this as working on extensions of the Curry-Howard correspondence relevant to applications of proof theory in mathematics and in proof assistant systems such as Coq. In particular, I contribute to structural proof theory as participant to the ProofCert project in the team Parsifal.

Publications | Formal Proofs and Software | Teaching | CV | Contact

*(28 June 2016)*Talk at Computability in Europe 2016 (CiE 2016)*(May 2016)*New version of arXiv:1502.04634*(January 2016)*New arXiv:1601.04876 on an arithmetical hierarchy for constructive logic (with Taus Brock-Nannestad)