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

- The exp-log normal form of types, arXiv paper -- Coq code
- An Intuitionistic Formula Hierarchy Based on High-School Identities (with Taus Brock-Nannestad), arXiv paper -- Coq code
*(28 June 2016)*Talk at Computability in Europe 2016 (CiE 2016)- Perspectives for proof unwinding by programming languages techniques, book chapter