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
[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
- A journey through Krivine's classical realizability (Part I / Part II), Seminário de Lógica Matemática, CMAFcIO, Lisbon, November 2020
- The benefits of sequent calculus, an introduction to the computational contents of sequent calculus and its benefits, given at the Logic Mentoring Worskhop, Vancouver, June 2019.
- Curry-Howard: unveiling the computational content of proofs, introductory talk for a public of mathematicians that I gave during the dynamics seminar of the IMERL, Montevideo, November 2018.
- Realizabilidad clásica y efectos colaterales: Extendiendo la correspondencia de Curry-Howard, a banner (in spanish) that I presented during the 2da jornada de reconocimiento a la ciencia organized by the Uruguayan Ministery of Education (Montevideo, December 2018).
[+] Realizability
- New Realizability with stateful computations for nonstandard analysis, at CSL 2021 , see also the video of the talk.
- Nonstandard analysis in Krivine realizability, workshop Days in Logic, Lisbon, January 2020
- Revisiting the duality of computation: an algebraic analysis of classical realizability models, workshop Facets of Realizability, Cachan, July 2019
- Realizability games for arithmetic formulas, CHoCoLa meeting, ENS Lyon, May 2015
- Realizabilidad clásica : una introducción, meeting organized by the INCO and the ORT, Montevideo, December 2013
[+] Dependent choice and classical logic
- A sequent calculus with dependent types for classical arithmetic, workshop on classical realizability, Marseille, June 2018
- Una prubea constructive del axioma de elección dependiente en lógica clásica (suite et fin), seminar of the logic team of the IMERL, Montevideo, March 2016
[+] Type theory
- Dependent Type Theory in Polarised Sequent Calculus, Deducteam seminar, February 2020.
- How delimited continuations can be used to define dependently typed CPS, TYPES 2018, Braga.
[+] Classical call-by-need
- New CPS translations & environments - A well-typed story, talk for the seminar of the Birmingham's Theory of Computation team, summarizing FOSSAC 18 & LICS 20 paper.
- A calculus of expandable stores. Continuation-and-environment-passing style translations, online talk for LICS 20. See also the companion paper above.
- Realizability Interpretation and Normalization of Typed Call-by-Need λ-calculus with Control, talk given at FOSSACS 18, Thessaloniki. See also the companion paper above.
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
2020-2021 (ÉNS de Lyon)
[+] Proofs & Programs
- See Colin Riba's page.
[+] L3
- See the corresponding pages on the Portail des Études.
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)
- la page du cours de Jean-Baptiste Yunés, Olivier Carton et Yann Régis-Gianas.
- TD1 : Conception de classes, énoncé
- TP1 : Conception de classes, énoncé
- TD2 : Domaines d'accès, associations de classes, encapsulation, énoncé
- TP2 : Domaines d'accès, associations de classes, encapsulation, énoncé
- TD3 : Héritage, énoncé
- TP3 : Héritage, énoncé
- TD4 : Héritage et interfaces, énoncé
- TP4 : Héritage et interfaces, énoncé
- TD5 : Un gros paquet d'erreurs, énoncé
- TP5 : Jouons, énoncé et fichiers
- TD6 : Un peu de classe astraite, énoncé
- TP6 : Quizz et plus, énoncé
- TD7 : , énoncé
- TP7 : , énoncé
- TD8 : I/O et Exceptions, énoncé
- TP8 : I/O et Exceptions, énoncé et fichiers
- TD9 : Types génériques et classes paramétrées, énoncé
- TP9 : Pattern observateur/observé, énoncé
- TD10 : Collections, énoncé
- TP10 : Collections, itérateurs, énoncé
- TD11 : Classes internes et pattern MVC, énoncé
- TP11 : Un mélangeur de couleurs, énoncé et fichiers
- TP11 : Révisions, énoncé
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)
- la page du cours de Ralf Treinen
- TP1 : Sed et expressions régulières, énoncé et fichiers
- TP2 : Automates en Java, énoncé et fichiers
- TP3 : JFLEX (analyse lexicale), énoncé et fichiers
- TP4 : Analyse syntaxique en Java, énoncé et fichiers
- TD5 : Grammaires LL1, énoncé
- TP6 : Analyse lexicale et syntaxique
- TP7 : Fichiers XML et OpenStreetMap, énoncé et fichiers
- TP8 : Expressions arithmétiques, énoncé et fichiers
2011-2012 (Lycée du parc)
[+] Option informatique (MP/MP*)
- TP1 : Remise en forme - - énoncé et template, corrigé
- TP2 : Graphes - énoncé, corrigé
- TP3 : λ-calcul et compilation - énoncé, corrigé
- TP4 : Seamcarving - énoncé et template, corrigé
- TP5 : Cryptographie par RSA - énoncé et template, corrigé
- TP6 : Arithmétique des polynômes - énoncé
- TP7 : Arbres binaires - énoncé
- TP8 : Fractales - énoncé et template
- TP9 : Automates - énoncé
- Préparation aux oraux d'info fondamentale :