Rencontre, 15 mai 2025

Rencontre, 3 avril 2025

Rencontre, 13 mars 2025

Rencontre, 6 février 2025

Rencontre, 21 novembre 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 octobre 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 septembre 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 juin 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 mai 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 avril 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 mars 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 janvier 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 décembre 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 novembre 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 octobre 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 septembre 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 juin 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 mai 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 mars 2023

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

Rencontre, 26 janvier 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 novembre 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 octobre 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 septembre 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 juin 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 mai 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 mars 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 mars 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 mai 2020

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

Rencontre, 13 mars 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 février 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 juin 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 mai 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 avril 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 mars 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 janvier 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 décembre 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 novembre 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 septembre 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 mai 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 avril 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 mars 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 février 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 décembre 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 novembre 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 octobre 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 juin 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 mai 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 avril 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 mars 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 février 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 janvier 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 novembre 2016

Rencontre, 9 novembre 2016