Welcome to my academic web page!

You can find here my work in **Logic**
and **Programming**, about the:

- computational content of choice axioms and of completeness theorems;
- meta-theory of intuitionistic logic, such an intuitionistic arithmetical hierarchy;
- formula and type isomorphism, canonical forms of proofs and functional programs;
- type-directed partial evaluation using dependently typed continuations;
- various proof formalizations in Coq and Agda, including one of historical interest: Zermelo's 1904 proof of the well-ordering theorem.

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

*(Aug 2021)*Demo paper Coqlex, an approach to generate verified lexers to be presented at ML 2021 (work with Wendlasida Ouedraogo and Lutz Strassburger)*(Jan 2020)*Wendlasida Ouedraogo starts his PhD thesis, co-supervised with Lutz Strassburger*(July 2019)*Talk at PLS12 in Anogeia, Crete, on Applications of the analogy between formulas and exponential polynomials to equivalence and normal forms*(May 2019)*The paper An Intuitionistic Formula Hierarchy Based on High-School Identities (**with Taus Brock-Nannestad**) was published in Mathematical Logic Quarterly*(January 2018)*Talk at EUTypes 2018 Working Meeting in Nijmegen, The Netherlands*(December 2017)*My Perspectives for proof unwinding by programming languages techniques was published in IfColog Journal of Logics and their Applications*(February 2017)*Talk at CHoCoLa, ENS Lyon*(January 2017)*Talk at 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017) on The exp-log normal form of types