I am Maître de Conférences in the I2M within the team Logique de la Programmation.
Previously, I have occupied an ATER (temporary teaching and research attaché) position in the LIP lab. I have occupied post-doc positions in the LSV lab (CNRS), supervised by Valentin Blot and in the INRIA team Gallinette with Guillaume Munch-Maccagnoni. Before that, I was a PhD student under the co-supervision of (in the IRIF laboratory, within the team πr²) and Alexandre Miquel (in the Mathematical Institute of the Faculty of Engineering of Montevideo).
I am mainly interested in the computational content of proofs, and especially in classical realizability. You will find below a list of documents in relation with my research work. As for the rest of this webpage content, it needs to be refreshed and should be back online soon enough I hope.
You can contact me via:
Publications and drafts
(see HAL deposits for extended papers with appendices)Journal papers
Conference proceedings
PhD. Thesis
- Classical realizability and side-effects
[pdf] Université Paris-Diderot & Universidad de la República, 2017.
Under the supervision of and .
More details and the companion Coq development are given here.
Manuscripts
As a student, I did several internships which lead to the writing of manuscripts, here are some of them.Selected talks
[+] Introductory talks
[+] Realizability
[+] Dependent choice and classical logic
[+] Type theory
[+] Classical call-by-need
Coq developments
Implicative algebras
You can find here a formalization of Alexandre Miquel's implicative algebras (see also the companion paper above) and of its disjunctive and conjunctive variants: https://gitlab.com/emiquey/ImplicativeAlgebras.
λµµ̃-calculus
During my PhD years, I formalized (for fun) Curien-Herbelin's λµµ̃-calculus, using Arthur Charguéraud's LN Library. It might not be up to date, feel free to ask me anything you need about it: https://framagit.org/emiquey/lambdamumutilde.
Teaching
2021-2022 - Licence MPCI
[+] Prog1 & Prog2
- Information sur AMETICE.
- Information sur AMETICE.