Publications

Articles

• “Upon This Quote I Will Build My Church Thesis” (LICS 2024)
• ∂ is for Dialectica (with Marie Kerjean, LICS 2024)
• Gardening with the Pythia (CSL 2022)
• Russian Constructivism in a Prefascist Theory (LICS 2020)
• The Fire Triangle: How to Mix Substitution, Dependent Elimination and Effects (with Nicolas Tabareau, POPL 2020)
• A Reasonably Exceptional Type Theory (with Hans Fehrmann, Nicolas Tabareau and Éric Tanter)
• Failure is Not an Option: An Exceptional Type Theory (with Nicolas Tabareau, ESOP 2018)
• An Effectful Way to Eliminate Addiction to Dependence (with Nicolas Tabareau, LICS 2017)
• Modèles de la théorie des types donnés par traduction de programme (with Simon Boulier and Nicolas Tabareau, JFLA 2017)
• The Next 700 Syntactical Models of Type Theory (with Simon Boulier and Nicolas Tabareau, CPP 2017)
• The Definitional Side of the Forcing (with Guilhem Jaber, Gabriel Lewertowski, Matthieu Sozeau and Nicolas Tabareau, LICS 2016)
• Classical by-need (with Alexis Saurin, ESOP 2016)
• A Functional Functional Interpretation (CSL-LICS 2014)
• Nécessité faite loi : de la réduction linéaire de tête à l'évaluation paresseuse (with Alexis Saurin, JFLA 2014)
• Un régime au concentré d'automate (JFLA 2013)

Talk slides

• Dialectica the Ultimate, 08/07/2024, TLLA 2024
• « Dans les Boyaux de mon Noyau », 19/03/2024, JNIM 2024
• « “A quote? In my type theory?” », 18/10/2023, Gallinette seminar on metaprogramming (Long version presented at Deducteam)
• « From Lost to the River: Embracing Sort Proliferation », 12/06/2023, TYPES 2023
• « Russian Constructivism in a Prefascist Theory », 08/07/2020, LICS 2020
• « An Authoritarian Approach to Presheaves », 05/06/2020, Birmingham Theory of Computation seminar
• « The Fire Triangle: How to Mix Substitution, Dependent Elimination and Effects », 13/01/2020, POPL 2020
• A Reasonably Exceptional Type Theory (ICFP 2019)
• Effects, Substitution and Induction: An Explosive Ménage à Trois (TYPES 2019)
• « Une théorie des types qui fait de l'effet » (Part 1, Part 2), 02/2019, JFLA 2019
• « Failure is Not an Option: The Curry-Howard-Shadok correspondence », 22/02/2018, PPS Seminar
• « Proof Assistants for Free », 24/01/2018, EUTypes meeting 2018
• « Taming Effects in a Dependent World », 14/11/2017, Journées Géocal-LAC 2017
• « A Parametric CPS to Sprinkle CIC with Classical Reasoning », 19/06/2017, LOLA 2017
• « An Effectful Way to Eliminate Addiction to Dependence », 31/01/2017, EUTypes-SSTT 2017
• « The Next 700 Syntactical Models of Type Theory », 17/01/2017, CPP 2017
• « Towards Ltac 2.0 », 08/06/2016, DeepSpec Workshop
• « Ltac Internals », 03/06/2016, Coq Implementors' Workshop
• « The Definitional Side of the Forcing », 24/05/2016, TYPES 2016
• « The Dialectica Translation of Type Theory », 24/05/2016, TYPES 2016
• « Classical by Need », 07/04/2016, ESOP 2016
• « A Survey of Coinduction in Coq », 18/06/2015
• « The Curry-Howard isomorphism for dummies » (INRIA Junior Seminar), 17/02/2015 [Video Recording]
• « Dialectique concrète et machines abstraites » (Journées PPS), 22/09/2014
• « Dialectica peut-elle casser des briques ? », 22/10/2013 (English version presented at Chocola)
• « Un régime au concentré d'automate » (JFLA), 06/02/2013
• « Ça dépend, ça dépasse », 14/11/2012
• « Double glueing and orthogonality », 23/11/2011

Drafts and abstracts

• “Proofs are programs” in MLTT (TYPES 2024)
• From Lost to the River: Embracing Sort Proliferation (TYPES 2023)
• Effects, Substitution and Induction: An Explosive Ménage à Trois (TYPES 2019)
• Ltac2: Tactical Warfare
• An Effectful Way to Eliminate Addiction to Dependence (TYPES 2017)
• The Definitional Side of the Forcing (TYPES 2016)
• The Dialectica Translation of Type Theory (TYPES 2016)
• Dialectica: From Gödel to Curry-Howard (TYPES 2014)

Notes

• Pursuing Shtuck
• Debunking Sheaves
• Presheaves as a Purified Effecful Call-by-Value Language
• Half a Syntactic Model to Prove Markov's Principle in CIC

PhD thesis

Thesis manuscript: A Materialist Dialectica (slides, summary)

Community

• PC member of the Coq Workshop 2019
• PC member of the Coq Workshop 2018
• PC member of TYPES 2018

Internships

• Étude de CTML : un ML en appel par nom avec opérateurs de contrôle (L3 internship, supervized by Olivier Laurent, in French)
• On the semantics of the Effect Calculus (first M1 internship, supervized by Masahito Hasegawa)
• Bisimulations d'un lambda-calcul polymorphe impératif en Coq (second M1 internship, supervized by Jacques Garrigue, in French)
• Double-glueing and Linear Logic (M2 internship, supervized by Olivier Laurent)