Welcome to my former research page (do not hesitate to contact me if you have a question about one of my articles).
I moved to the industry in october 2022 and am currently looking for a position as a software engineer and/or anything that involves (non-elementary) maths! You may find my resume here and my LinkedIn profile there.
This page should welcome soon some other material beyond computer science :)

The last academic position I occupied was a post-doc in the Deducteam in the LMF (Laboratoire Méthodes Formelles), located in ENS Paris-Saclay (south of Paris), under the supervision of Chantal Keller and Valentin Blot.
There, I was part of the development team of the Coq module Sniper, which help do some proof automation in Coq.
I used to be a Phd student at IRIF (Paris) and a post-doc in the Gallinette Inria team (Nantes).

Here were my main interests (some still are!)

• Quantitative intersection type systems, which bring information on how many steps are needed to evaluate a program to its final value.
• Infinitary calculi and coinduction, which allow capturing asymptotic behaviors of programs
• Lambda-Mu calculus (and calculi based on classical logic, which enable handling control operator)
• Semantics of the pure lambda-calculus
• Proofs of normalization in higher-order type theory with dependent types
• Automating the proof assistant Coq and conversely, using Coq to certify external softwares.
• Metaprogramming, in particular with MetaCoq (which is in good part developped in Gallinette) and now Coq Elpi.

A@B.com where A = pvial2401 and B = gmail.com