Before, I studied computer science and mathematics at Ecole Normale Supérieure and got a master degree from Master Parisien de Recherche en Informatique. You can have a look at my CV (Version française).
I am working on term representations based on proof theory.
Terms (or expressions) are essential in many different settings: mathematical proofs, programming languages, proof assistants and so on. Proof theory has been widely used to motivate the design of term structures via notably the Curry-Howard correspondence.
The goal of my PhD project is to build a logical framework based on proof theory to describe/unify/justify different term representations, in the hope that proof-theoretic considerations will on one hand provide careful and formal descriptions of term structures and on the other hand give us more insights on terms.
Instead of using proof systems such as Gentzen’s natural deduction and sequnet calculus, we use the focused proof system LJF in order to give more structure to proofs. The notion of polarization gives the flexibility to construct differents forms of proofs, which is a desirable feature since we want to describe different term structures in our system.
Some problems I am thinking about:
How can terms (proofs) built using different polarization interact with each other?
How can terms (proofs) built using different axioms interact with each other?
What is the “meaning” of a term from a purely logical point of view?
APLL, an automated prover for linear logic designed and implemented by me years ago.
My brother is a freelance illustrator, check out his works here.
Publications & preprints
LFMTP 2022A positive perspective on term representation: work in progress2022
LICS 2021Combinatorial Proofs and Decomposition Theorems for First-order LogicIn 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2021