photo I am currently ATER (temporary teaching and research attaché) at the ÉNS de Lyon in the LIP lab.

Previously, 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, which is in french, you can access it by clicking some of the links above.

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
    [HAL, 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.

Selected talks

[+] Introductory talks

[+] Classical 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

2016-2017 (Université Paris-Diderot)

[+] Élements d'algorithmique II (EA4)

  • Tous les documents se trouvent sur le moodle de l'université.

2015-2016 (Université Paris-Diderot)

[+] Programation orientée objet et interfaces graphiques (POO3)

2014-2015 (Université Paris-Diderot)

[+] Introduction à la programmation (IP1)

  • la page du cours de Yann Régis-Gianas.

[+] Analyse de données structurées (ADS4)

2011-2012 (Lycée du parc)

[+] Option informatique (MP/MP*)