Rencontre, 25 June 2026

• Francesco Gavazzo (Università di Padova, It), TBA

Rencontre, 28 May 2026

• Nuria Brede (IRIF), On a generic approach to constructive reverse mathematics
• Bruno da Rocha Paiva (University of Birmingham), Internalising effectful forcing in System T
• Sam van Gool (ENS Paris Saclay), Ultraconvergence spaces

Rencontre, 30 April 2026

• Simon Castellan (Épicure, INRIA), Social studies of science as inspiration for research in PL
• Thiago Felicissimo (Galinette, INRIA), Definitional Proof Irrelevance Made Accessible
• Niyousha Najmaei (LIX, École Polytechnique), From Semantics to Syntax: A Type Theory for Comprehension Categories

Rencontre, 2 April 2026

• Mariangiola Dezani (Unviersità di Torino), Intersection Type Galore
• Stephanie Weirich (University of Pennsylvania), Tracking how dependently typed functions use their arguments
• Steve Zdancewic (University of Pennsylvania), Vellvm: Formal Verification of LLVM IR Code

Rencontre, 12 March 2026

• Davide Barbarossa (LIP, ENS de Lyon), Computational interpretations of logic : the case of Dialectica
• Jean Krivine (CNRS, IRIF), Reversible Computations are Computations
• Éléonore Mangel (IRIF), Classical notions of computation and the Hasegawa-Thielecke theorem

Rencontre, 5 February 2026

• Jui-Hsuan Wu (Ray) (LIP, ENS de Lyon), Non-Wellfounded Derivations for Intersection Subtyping with Fixpoints
• Raphaëlle Crubillé (LIS, Université Aix-Marseille), Interpreting De Finetti's Theorem in the Category of Integrable Cones
• Morgan Rogers (LIPN, Université Sorbonne Paris Nord), What is a monoid?

Rencontre, 26 June 2025

• Vikraman Choudhury (Università di Bologna), The Duality of λ-Abstraction
• Danielle Marshall (University of Glasgow), Linearity, Uniqueness, Ownership: An Entente Cordiale
• Elaine Pimentel (University College London), Alternative Semantic Views of Modality: From the Modal Cube to Linear Logic

Rencontre, 15 May 2025

• Daniel Gratzer (Aarhus University), Modal dependent type theory and synthetic category theory
• Elies Harington (LIX and LIPN), ∞-categorical models of linear logic : higher polynomials, higher species
• Hiroshi Unno (Research Institute of Electrical Communication, Tohoku University), Refinement Types and Higher-Order Model Checking for Algebraic Effects and Handlers

Rencontre, 3 April 2025

• Chase Ford (Universiteit Leiden, NL), Algebraic reasoning in locally presentable categories
• Elies Harington [THE TALK IS POSTPONED TO A LATER CHOCOLA MEETING] (LIX and LIPN), THE TALK IS POSTPONED TO A LATER CHOCOLA MEETING (was: ∞-categorical models of linear logic : higher polynomials, higher species)
• Josselin Poiret [THE TALK IS POSTPONED TO A LATER CHOCOLA MEETING] (Galinette, INRIA), THE TALK IS POSTPONED TO A LATER CHOCOLA MEETING (was: Sort Polymorphism for Proof Assistants)

Rencontre, 13 March 2025

• Victoria Barrett (Partout, INRIA), Subatomic logic and eversion in deep inference
• Elena di Lavore (University of Oxford (UK)), Kleene-cartesian bicategories for program logics.
• Maribel Fernandez (King's College (UK)), Specifying Calculi with Binders in Rewriting Logic

Rencontre, 6 February 2025

• Justin Hsu (Cornell University), Type Systems for Numerical Error Analysis
• Shin-Ya Katsumata (Kyoto Sangyo University), Codensity liftings and their applications to semantics
• Valentin Maestracci (Université Aix-Marseille), The Lambda Calculus can be Quantified

Rencontre, 21 November 2024

• Isabelle Collet (Université de Genève), Femmes et numérique : pratiques égalitaires, dispositifs inclusifs
• Adrienne Lancelot (IRIF - Université Paris Cité), Interaction Equivalence
• Théo Winterhalter (Deducteam, INRIA), Dependent Ghosts Have a Reflection for Free

Rencontre, 17 October 2024

• Jonas Frey (LIPN, Université Sorbonne Paris-Nord), The shape of contexts
• Dominik Kirst (IRIF - Université Paris Cité), Separating Markov’s Principles in Constructive Type Theories
• Pierre-Marie Pédrot (Galinette, INRIA), Upon This Quote I Will Build My Church Thesis

Rencontre, 19 September 2024

• Clovis Eberhart (NII, Japon), A Compositional Approach to Verification Models
• Zeinab Galal (Università di Bologna), Combining fixpoint and differentiation theory
• Vincent Moreau (IRIF - Université Paris Cité), Profinite trees, through monads and the lambda-calculus

Rencontre, 27 June 2024

• Pierre Clairambault (LIS, Marseille), An Analysis of Symmetry in Quantitative Semantics
• Aloÿs Dufour (LIPN, Université Sorbonne Paris-Nord), Böhm and Taylor for all
• Matthieu Piquerez (Galinette, INRIA), Machine-Checked Categorical Diagrammatic Reasoning

Rencontre, 23 May 2024

• Victor Arrial (IRIF), Genericity Through Stratification
• Stelios Tsampas (FAU Erlangen-Nürnberg), Logical Relations in Higher-Order Mathematical Operational Semantics
• Maaike Zwart (IT University of Copenhagen), What Monads Can and Cannot Do With a Bit of Extra Time

Rencontre, 4 April 2024

• Peio Borthelle (Université Savoie Mont Blanc), Operational Game Semantics, certified in Coq
• Brigitte Pientka (McGill University), A Framework for Certified Meta-programming
• Christine Tasson (ISAE-SUPAERO), Density-Based Semantics for Reactive Probabilistic Programming

Rencontre, 14 March 2024

• Rémi di Guardia (LIP, ENS de Lyon), Retractions in Multiplicative Linear Logic
• Thomas Ehrhard (CNRS, Université Paris Cité), Intégration dans les cônes
• Luc Pellissier (Université Paris-Est Créteil), Droit expérimental des algorithmes publics

Rencontre, 25 January 2024

• Emmanuel Beffara (Univ. Grenoble Alpes), Concurrent Realizability on Conjunctive Structures
• Marie Kerjean (LIPN, Université Sorbonne Paris-Nord), DiLL est dans Laplace
• Gabriel Scherer (Parsifal, INRIA), Constructor unboxing

Rencontre, 14 December 2023

• Lionel Vaux Auclair (Université Aix-Marseille), Extensional Taylor Expansion
• Marianna Girlando & Sonia Marin (University of Amsterdam and University of Birmingham), Decidability of intuitionistic S4: a proof theoretic algorithm
• Paige Randall North (Utrecht University), Coinductive control of inductive data types

Rencontre, 16 November 2023

• Cyril Cohen (INRIA), Trocq: Proof Transfer for Free, With or Without Univalence
• Simon Forest (Université Aix-Marseille), Thin spans and their modelling of rigid intersection types
• Morgan Rogers (LIPN, Université Sorbonne Paris-Nord), A topos theory travel guide

Rencontre, 19 October 2023

• Tom Hirschowitz (CNRS, Université Savoie Mont Blanc), A categorical framework for congruence of applicative bisimilarity
• Alexandre Moine (Cambium, INRIA), Diamonds Are Forever: Reasoning about Heap Space in a Concurrent and Garbage Collected Language
• Hugo Paquet (LIPN, Université Sorbonne Paris-Nord), Element-free probability distributions and Bayesian clustering

Rencontre, 28 September 2023

• Antoine Allioux (IRIF), Higher Structures in Homotopy Type Theory
• Lison Blondeau-Patissier (Aix-Marseille), Strategies as Resource Terms, and their Categorical Semantics
• William Simmons (Oxford University (UK)), An exact logic for compatibility of higher-order causal structures

Rencontre, 15 June 2023

• Bryce Clarke (Partout team, INRIA), Reflections on delta lenses
• Aymeric Walch (IRIF), Cartesian Coherent Differential Categories
• Noam Zeilberger (École Polytechnique), Parsing as a lifting problem and the Chomsky-Schützenberger representation theorem

Rencontre, 11 May 2023

• Axel Kerinec (LIPN), Why Are Proofs Relevant in Proof-Relevant Models?
• Adrienne Lancelot (LIX, École Polytechnique), Normal Form Bisimulations by Value
• Gabriele Vanoni (INRIA Sophia Antipolis), Monadic Intersection Types

[Rencontre] The event is canceled, 9 March 2023

• Peter Dybjer (Chalmers Univ. (Sweden)), Generalized Algebraic Theories and Categories with Families
• Axel Kerinec (LIPN), TBA
• Gabriele Vanoni (INRIA), TBA

Rencontre, 26 January 2023

• Zeinab Galal (LIP6, Sorbonne Université), Bidimensional fixpoint operators
• Meven Lennon-Bertrand (Cambridge Univ. (UK)), Bidirectional typing is not just an implementation technique
• Yannick Zakowski (INRIA (Lyon)), Monadic Definitional Interpreters as Formal Semantic Models of Computations

Rencontre, 24 November 2022

• Giulio Guerrieri (LIS, Aix-Marseille Université), The theory of call-by-value solvability
• Hugo Herbelin (INRIA), Computing with Gödel’s completeness theorem: Weak Fan Theorem, Markov’s Principle and Double Negation Shift in action
• Daniela Petrisan (IRIF), Semialgebras and Weak Distributive Laws

Rencontre, 20 October 2022

• Martin Baillon (Gallinette, LS2N), Gardening with the Pythia, A model of continuity in a dependent setting
• Marie Fortin (IRIF, CNRS), FO = FO^3 for Linear Orders with Monotone Binary Relations
• Tito Nguyễn (LIP, ENS de Lyon), A transducer model for simply typed λ-definable functions

Rencontre, 22 September 2022

• Romain Couillet (Université Grenoble-Alpes), Pourquoi et comment démanteler l'IA et le numérique?
• Claudia Faggian (CNRS - IRIF), Bayesian Networks and Proof Nets: Curry-Howard meets Bayes
• Guillaume Geoffroy (IRIF), A first-order completeness result about characteristic Boolean algebras in classical realizability

Rencontre, 2 June 2022

• Valentin Blot (INRIA), A direct computational interpretation of second-order arithmetic via update recursion
• Louise Dubois de Prisque (LMF, Inria), Sniper, a general proof automation tactic in Coq
• Yannick Forster (Gallinette, Nantes), Synthetic Computability in Constructive Type Theory

Rencontre, 5 May 2022

• Nathanaëlle Courant (INRIA), Testing convertibility in parallel
• Gianluca Curzi (Università di Torino), Cyclic implicit complexity
• Farzad Jafarrahmani (IRIF), Linear logic with fixpoints from a Curry-Howard perspective.

Rencontre, 31 March 2022

• Abhishek De (IRIF), Provability of linear logic with fixed points
• Cristina Matache (Oxford University, UK), A unified treatment of concrete sheaf models for higher-order recursion
• Federico Olimpieri (University of Leeds, UK), Categorifying graph models of lambda calculus

Rencontre, 10 March 2022

• Marie Kerjean (CNRS - LIPN), ∂ is for Dialectica
• Denis Kuperberg (CNRS - LIP), Positive First-order Logic on Words and Graphs
• Loïc Pujet (Gallinette, INRIA), Extensionality in intensional type theory

Rencontre, 14 May 2020

• Neel Krishnaswami (University of Cambridge (UK)), TBA
• Cristina Matache (Oxford University (UK)), Program Equivalence for Algebraic Effects and Higher-order Functions

Rencontre, 13 March 2020

• Amina Doumane (CNRS, ENS de Lyon), Completeness for Identity-free Kleene Lattices
• Giulio Guerrieri (University of Bath (UK)), Factorization, Normalization and all that.
• Damiano Mazza (CNRS, Univ. Paris 13), Automatic Differentiation in PCF

Rencontre, 6 February 2020

• Cyrille Chenavier (Johannes Kepler University (Linz, Austria)), Topological rewriting systems applied to standard bases and syntactic algebras
• Damiano Mazza (CNRS, Univ. Paris 13), Backpropagation in the Simply Typed Lambda-calculus with Linear Negation
• Luc Pellissier (INRIA and École Polytechnique), Glueability of resource proof-structures: inverting the Taylor expansion

Rencontre, 6 June 2019

• Ohad Kammar (University of Edinburgh), A tutorial on quasi-Borel spaces
• Jérémy Ledent (LIX, École Polytechnique), Geometric semantics for asynchronous computability
• Lutz Strassburger (INRIA Saclay and LIX, École Polytechnique), Introduction to Combinatorial Proofs

Rencontre, 9 May 2019

• Radu Mardare (Aalborg University (DK)), Non-standard semantics for stochastic computational phenomena
• Daniela Petrisan (IRIF, Univ. Paris Diderot), Up-To Techniques for Behavioural Metrics via Fibrations
• Mathys Rennela (LIACS, Leiden University, NL), Operator algebras in categorical quantum foundations

Rencontre, 4 April 2019

• Raphaëlle Crubillé (IRIF, Univ. Paris Diderot), Probabilistic Stable Functions on Discrete Cones are Power Series.
• Xavier Leroy (Collège de France, INRIA), Formal verification of a static analyzer: abstract interpretation in type theory
• Ludovic Patey (CNRS, Institut Camille Jordan), Introduction to reverse mathematics

Rencontre, 14 March 2019

• Ambroise Lafont (IMT Atlantique), Higher-order Arities, Signatures and Equations via Modules
• Étienne Miquey (Gallinette, INRIA), A constructive proof of dependent choice in classical arithmetic via memoization
• Filip Sieczkowski (University of Wrocław), Abstraction and equational reasoning for algebraic effects and handlers

Rencontre, 24 January 2019

• Aurore Alcolei (ENS de Lyon), Resource-tracking concurrent games
• Paul-André Melliès (CNRS - Univ. Paris Diderot), Template games: a homotopy model of differential linear logic
• Andreas Nuyts (KU Leuven (Be)), Degrees of Relatedness

Rencontre, 13 December 2018

• Tom Hirschowitz (CNRS - Univ. Savoie Mont Blanc), Familial monads and structural operational semantics
• Lê Thành Dũng Nguyễn (Université Paris 13), Around finite semantics for second-order multiplicative linear logic
• Paolo Pistone (Tübingen Univ. (DE)), Coends and proof equivalence in second order multiplicative linear logic

Salidou day, 15 November 2018

• Flavien Breuvart (Université Paris 13), Graded Types Parametricity : Principles and Application to Abstract Interpretation
• Xavier Leroy, Leçon inaugurale au Collège de France
• Shane Mansfield (Univ. of Oxford), An overview of empirical models
• Éric Tanter (Universidad de Chile & Inria Paris), Abstracting Gradual Typing: Principles and Application to Gradual Parametricity

Rencontre, 20 September 2018

• Henning Basold (CNRS - ENS de Lyon), Foundations for Corecursive Proof Search with Horn Clauses
• Guillaume Geoffroy (Institut de Mathématiques de Marseille), Connecting degrees of parallelism and Boolean algebras through classical realizability
• Thomas Streicher (Univ. Darmstadt (DE)), How Unique are Ground Models

Rencontre, 17 May 2018

• Florian Faissole (LRI), Synthetic topology in homotopy type theory for probabilistic programming
• Luca Padovani (Università di Torino), Mailbox Types for Unordered Interactions
• Tarmo Uustalu (Reykjavik University and Tallinn Univ. of Technology), A Coalgebraic View of Bar Recursion and Bar Induction

Rencontre, 12 April 2018

• Jean-Simon Lemay (University of Oxford (UK)), Differential Algebras for Differential Categories
• Jamie Vicary (University of Oxford (UK)), Practical higher-dimensional algebra
• Glynn Winskel (Cambridge University, UK), Distributed Probabilistic Strategies

Rencontre, 15 March 2018

• Bérénice Delcroix-Oger (IRIF, Univ. Paris Diderot), Why operads can be seen as enhanced species and what they are used for.
• Marcelo Fiore (University of Cambridge, UK), An Algebraic Combinatorial Approach to the Abstract Syntax of Opetopic Structures
• Samuel Mimram (École Polytechnique), Mechanized tools for higher categories

Rencontre, 8 February 2018

• Thomas Ehrhard (IRIF, Univ. Paris Diderot), Stable and measurable functions on positive cones: a model of probabilistic functional languages with continuous types
• Justin Hsu (University College London, UK), From Couplings to Probabilistic Relational Program Logics
• Prakash Panangaden (Mc Gill University, Canada), Quantitative Equational Logic

Rencontre, 14 December 2017

• Jean Krivine (IRIF, Univ. Paris Diderot), Incremental Update for Graph Rewriting
• Kenji Maillard (INRIA), F*, from practice to theory
• François Pottier (INRIA), Looking back on Mezzo: experience and metatheory

Rencontre, 9 November 2017

• Jules Chouquet (IRIF, Univ. Paris Diderot), A result concerning the size of proof-nets, and two applications
• Laura Fontanella (I2M, Aix-Marseille), Realizability: from Curry-Howard to forcing
• Thomas Seiller (DIKU, Univ. Copenhagen), Towards a geometric theory of computation(al complexity)

Rencontre, 12 October 2017

• André Joyal (Univ. Québec à Montréal), Opérades et 2-géométrie algébrique
• Damiano Mazza (CNRS, LIPN), A Tour Around Polyadic Approximations
• Luc Pellissier (ENS de Lyon), Linear approximations, intersection types and the Grothendieck construction

Rencontre, 29 June 2017

• Valentin Blot ( Queen Mary University of London), An interpretation of system F through bar recursion
• Marco Gaboardi (University at Buffalo, SUNY), A semantic account of metric preservation in presence of probabilities.
• Marie Kerjean (IRIF), Smooth models of Differential Linear Logic

Rencontre, 11 May 2017

• Paul Blain Levy (University of Birmingham), Contextual isomorphisms
• Pierre-Marie Pédrot (University of Ljubljana), An Effectful Way to Eliminate Addiction to Dependence
• Christine Tasson (IRIF, Univ. Paris Diderot), Probabilistic Call by Push Value

Rencontre, 13 April 2017

• Jérémie Chalopin (Université Aix-Marseille), Un contre-exemple à la conjecture de Thiagarajan sur les structures d'évènements régulières
• Thomas Leventis (Institut de Mathématiques de Marseille), Full abstraction of the probabilistic Böhm trees
• Pierre-Yves Strub (École Polytechnique), Proving Differential Privacy via Probabilistic Couplings

Rencontre, 9 March 2017

• Matteo Mio (CNRS, Lyon), Riesz Modal Logic for Markov Processes
• Hugo Paquet (Cambridge), Concurrent game semantics for Probabilistic PCF and relational collapse
• Benoît Valiron (CentraleSupélec & LRI), A Geometry of Interaction for Quantum Computation

Rencontre, 9 February 2017

• Danko Ilic, Exp-log normal form of types and formulas
• Olivier Laurent (CNRS, ENS de Lyon), On the Proof Theory of BCD Intersection Subtyping
• Gabriel Scherer (Northeastern University, Boston), Full abstraction for language design

Rencontre, 12 January 2017

• Pierre Pradic (ENS de Lyon), The Logical Strength of Büchi's Decidability Theorem
• Christophe Raffalli (Univ. Savoie Mont Blanc), About SubML
• Lionel Vaux (Univ. Aix-Marseille), Normaliser le développement de Taylor des λ-termes

Rencontre, 10 November 2016

Rencontre, 9 November 2016