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:

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.

Content

• Contact
• Publications
• Talks
• Teaching