Publications and drafts

Journal papers

Conference proceedings

Notes / In preparation

• 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).

• 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

• 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

• 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.

• 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.