This web page lists my research in Mathematical Logic and Theoretical Computer Science.

Since August 2016, I work in the industry, but do let me know if you have some interesting research proposal.

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.

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

*(October 2016)*The exp-log normal form of types, accepted to POPL 2017 -- 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