photo 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

Notes / In preparation

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.


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:


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:


2021-2022 - Licence MPCI

[+] Prog1 & Prog2