I am currently a master student in Computer Science at
École Normale Supérieure. I am particularly interested in
logic, programming language theory, and verification.
2018 Master 1 in Computer Science, École Normale Supérieure and MPRI , Paris, France
2017 - 2018 Licence 3 (B.Sc.) in Computer Science, École Normale Supérieure and Paris Diderot University, Paris, France
2017 Admitted to École Normale Supérieure, Paris, France.
2015 - 2017 CPGE, Lycée Janson-de-Sailly, Paris, France
Proof theory, Lambda calculus, Functional programming, Type theory, Automated theorem proving, Verification.
APLL : a focusing-based Automated Prover for Linear Logic
This prover for linear logic gives users the possibility of generating proof certificates that guarantee the validity of proofs by using the proof assistant Coq and the Yalla library.
There is a web interface under construction.
Here are the slides from my talk at the workshop on "Machine Proofs of Linear Logic". You can find more details here.
- APLL : a focusing-based Automated Prover for Linear Logic