Welcome to my research page.
I am a post-doc in the Deducteam in the newly formed LMF (Laboratoire Méthodes Formelles), located in Saclay (south of Paris).
I work on the SMTCoq project under the supervision of Chantal Keller and Valentin Blot. I used to be a Phd student at IRIF (Paris) and a post-doc in the Gallinette Inria team (Nantes).
You may find here a short
- June 2020: my article "Persistent and Consuming Types for Classical Logic" (joint work with Delia Kesner) was accepted at Lics'2020, which will occur online due to the Covid-19 pandemic
- Quantitative Intersection Type Systems
- Infinitary Calculi and Coinduction
- Lambda-Mu Calculus (and Calculi based on Classical Logic)
- Semantics of Pure Lambda Calculus
- Proofs of normalization in higher-order type theory with dependent types
- Certification of SMT solvers.
- Metaprogramming (in particular with MetaCoq).