| 2022-05-19 | Félix Loubaton | Univalence dans la catégorie des catégories |
| 2022-05-12 | Filippo Bonchi | Deconstructing Tarski's calculus of relations with Tape diagrams |
| 2022-05-05 | | Chocola à Lyon |
| 2022-03-31 | | Chocola à Lyon |
| 2022-03-24 | William Troiani | Proof nets, rings, and ideals |
| 2022-03-17 | Paul-André Melliès | Les jeux de gabarit, un modèle homotopique de la logique linéaire différentielle |
| 2022-03-03 | Lê Thành Dũng Nguyễn | Automates implicites en λ-calcul typé |
| 2022-01-13 | Davide Catta | Sémantique des jeux pour la logique modale CK |
| 2021-12-16 | Kostia Chardonnet | Geometry of Interaction for ZX-Diagrams |
| 2021-12-09 | Rémy Cerda | Développement de Taylor en λ-calcul infinitaire, suite |
| 2021-11-25 | Rémy Cerda | Développement de Taylor en λ-calcul infinitaire |
| 2021-11-18 | Ugo Dal Lago | On counting quantifiers and randomised computation |
| 2021-11-18 | Paul-André Melliès | Template games: a categorical combinatorics of scheduling and synchronisation |
| 2021-09-30 | Boris ENG | Une lecture technique de la syntaxe transcendantale |
| 2021-09-16 | Lison Blondeau-Patissier | Injectivité positionnelle pour les stratégies innocentes |
| 2021-09-09 | Thomas Ehrhard | Coherent differentiation |
| 2021-07-08 | Wesley Fussner | Sémantiques relationnelles et traductions modales pour Generalized Basic Logic |
| 2021-06-24 | Pierre Clairambault | The concurrent games abstract machine |
| 2021-06-10 | Giulio Guerrieri | Gluing resource proof-structures: inhabitation and inverting the Taylor expansion |
| 2021-05-27 | Guilhem Jaber | Compositional relational reasoning via operational game semantics |
| 2021-04-29 | Ambroise Lafont | Spécification mathématique de langages de programmation via les monades et leurs modules |
| 2021-04-15 | Étienne Miquey | Evidenced frames: a unifying framework broadening realizability models |
| 2021-04-01 | Giulio Guerrieri | Gluing resource proof-structures: inhabitation and inverting the Taylor expansion |
| 2021-03-18 | Simon Forest | Une extension du cadre de Batanin pour les catégories supérieures |
| 2021-01-21 | Raphaëlle Crubillé | On higher-order cryptography - Raphaëlle Crubillé |
| 2021-01-07 | Luidnel Maignan | The Bicategory of “Open Functors” and its Friends – Luidnel Maignan |
| 2020-11-26 | Christine Tasson | A multicategorical approach to mixed linear-non-linear substitution - Christine Tasson |
| 2020-11-12 | Lionel Vaux Auclair | Un groupoïde d’arbres de permutations (suite) |
| 2020-10-08 | Lionel Vaux Auclair | Un groupoïde d’arbres de permutations |
| 2020-07-02 | Peter Hines | Finding Resolution in unexpected places: Girard's formula outside its usual setting |
| 2020-02-13 | Thibaut Benjamin | Théorie des types pour les oméga-catégories faibles |
| 2019-12-05 | Mauricio Guillermo | Un programme d'algebrisation pour la réalisabilité ? (annulé) |
| 2019-11-28 | Léonard Guetta | Homologie des infini-catégories strictes |
| 2019-11-21 | Luigi Santocanale | On discrete idempotent paths |
| 2019-10-24 | Karoliina Lehtinen | Quasi-polynomial techniques for parity games and and other problems |
| 2019-09-12 | Cyrille Chenavier | Systèmes de réécriture topologiques appliqués aux bases standards et aux algèbres syntaxiques |
| 2019-07-11 | Zeinab Galal | Rigid species and normal functors over groupoids |
| 2019-07-04 | Pierre Hyvernat | Checking correctness for recursive definitions with mixed inductive and coinductive types |
| 2019-06-20 | Charles Grellois | Sur la terminaison des programmes probabilistes récursifs d'ordre supérieur |
| 2019-05-23 | Aurore Alcolei | Concurrent Games with side-information |
| 2019-05-02 | Marie Kerjean | Polarized models of Differential Linear Logic |
| 2019-04-25 | Raphaëlle Crubillé | Probabilistic stable functions on discrete cones are power series |
| 2019-03-29 | Guillaume Geoffroy | Réalisabilité classique : nouveaux outils et applications |
| 2019-03-28 | Thomas Streicher | Simplicial into cubical |
| 2019-03-21 | Luigi Santocanale | Quantales MIX *-autonomes et l'ordre faible continu |
| 2019-03-07 | Lionel Vaux Auclair | Combinatoire de l’élimination des coupures de MLL, et une application au développement de Taylor de MELL |
| 2019-02-28 | Claudia Faggian | Lambda Calculus and Probabilistic Computation |
| 2019-02-14 | Laura Fontanella, Guillaume Geoffroy | Un modèle de réalisabilité pour une version faible de l'axiome du choix (∀α.AC_α) |
| 2019-01-17 | Christophe Lucas | Towards a Proof Theory of the Riesz Modal Logic |
| 2019-01-10 | Dimitri Ara | Titre à préciser - Dimitri Ara |
| 2018-12-20 | Pierre Vial | Non idempotent typing, upper bounds and exact length in the lambda and in the lambda-mu-calculus |
| 2018-12-06 | Victor Chepoi | Matroïdes et leur graphes des bases |
| 2018-11-29 | Luc Pellissier | Linear Implicative Algebras, towards a BHK interpretation of linear logic |
| 2018-11-22 | Zeinab Galal | Connecting models of differential linear logic with reloids |
| 2018-10-11 | Thomas Ehrhard | Sémantique dénotationnelle de la logique linéaire avec plus petits et plus grands points fixes de types |
| 2018-10-04 | Giulio Manzonetto | Revisiting Call-by-value Bohm trees in light of their Taylor expansion |
| 2018-09-27 | Jules Chouquet | Une application de l’élimination parallèle des coupures en logique linéaire multiplicative sans unités au développement de Taylor des réseaux de preuves |
| 2018-09-13 | Tito Nguyen | Évaluation sémantique en logique linéaire élémentaire |
| 2018-09-06 | Etienne Miquey | The algebraic structure of classical realizability models |
| 2018-07-05 | Valentin Blot | Extensional and intensional semantic universes: a denotational model of dependent types |
| 2018-06-28 | Dimitri Ara | Joint et tranches ∞-catégoriques |
| 2018-06-21 | Maxime Lucas | Higher dimensional rewriting and cubical categories |
| 2018-06-14 | Pierre Clairambault | The true concurrency of Herbrand's theorem |
| 2018-06-07 | Pierre Vial | Representing permutations without permutations, or the expressive power of sequence types |
| 2018-04-26 | Andrea Gagna | Petites catégories comme modèles des types d'homotopie |
| 2018-04-19 | Alexis Saurin | Logical by-need |
| 2018-04-05 | Amina Doumane | Completeness for identity-free Kleene lattices |
| 2018-03-29 | Eduard Balzin | Les familles de catégories en géométrie et algèbre |
| 2018-03-08 | Andrea Gagna | Les petites catégories comme modèles des types d'homotopie (2ème partie) |
| 2018-02-22 | Assia Mahboubi | Une preuve assistée par ordinateur de l'irrationalité de zeta(3) |
| 2018-02-15 | Giulio Manzonetto | Refutation of Sallé's Longstanding Conjecture |
| 2018-02-08 | Andrea Gagna | Les petites catégories comme modèles des types d'homotopie |
| 2018-01-25 | Zeinab Galal | Espèces de structures et λ-calcul différentiel |
| 2018-01-18 | Hadrien Batmalle | Préservation de propriétés du modèle de départ en réalisabilité classique |
| 2018-01-11 | Michael Puschnigg | Toute algèbre à division sur les réels est de dimension 1, 2, 4 ou 8 (2ème partie) |
| 2017-12-21 | Clovis Eberhart | Une théorie des modèles de jeux |
| 2017-12-07 | Pierre Pradic | A realizability notion for MSO over ω |
| 2017-11-30 | Olivier Laurent | Une promenade entre logiques linéaires classiques et intuitionnistes |
| 2017-11-23 | Michael Puschnigg | Toute algèbre à division sur les réels est de dimension 1, 2, 4 ou 8 |
| 2017-11-16 | Maxime Lucas | La géométrie cubique de la réécriture de dimension supérieure |
| 2017-10-19 | Laura Fontanella | Grands cardinaux et compacité |
| 2017-09-28 | Patrick Dehornoy | La théorie des ensembles cinquante ans après Cohen |
| 2017-09-21 | Charles Grellois | Two type-theoretic approaches to probabilistic termination |
| 2017-06-22 | Victor Chepoi | Un contre-exemple à la conjecture de Thiagarajan sur les structures d'évènements régulières |
| 2017-06-15 | Luc Pellissier | Linear approximations, fibrations, intersection types |
| 2017-05-30 | Simon Henry | Théorie homotopique des types et modèles algébriques pour les infinis catégories et groupoïdes |
| 2017-05-30 | Edoardo Lanari | Globular models for weak higher dimensional structures |
| 2017-05-23 | Matteo Acclavio | Syntaxe et sémantique des diagrammes de preuve |
| 2017-05-04 | Cyrille Chenavier | Opérateurs de réduction et complétion de systèmes de réécriture linéaires |
| 2017-03-30 | Tom Hirschowitz | Shapely monads and analytic functors |
| 2017-03-23 | Pierre Vial | The complete unsoundness of coinductive intersection types (and how to escape it) |
| 2017-03-21 | Gérard Berry | Logique intuitionniste et stabilisation dans les circuits électroniques |
| 2017-03-16 | Domenico Ruoppolo | Relational graph models and observational theories |
| 2017-03-02 | Anupam Das | Monotonicity in Logic and Complexity |
| 2017-02-16 | Rodolphe Lepigre | Proofs of programs and subtyping in PML2 |
| 2017-02-02 | Claudia Faggian | The geometry of parallelism: probabilistic and quantum effects |
| 2017-01-26 | Gabriel Scherer | Deciding simply-typed equivalence with sums and the empty type |
| 2016-12-15 | Lorenzo Tortora de Falco | Remarques sur le développement de Taylor des réseaux |
| 2016-12-14 | Willem Heijltjes | Conflict nets: Locally canonical MALL proof nets |
| 2016-12-14 | Matteo Acclavio | Réécriture de diagrammes : applications à la théorie des catégories et à la théorie de la démonstration - Matteo Acclavio |
| 2016-12-08 | Antonino Salibra | The geometry of logic, algebra and computation |
| 2016-11-24 | Matteo Acclavio | Diagrammes de preuve pour la logique linéaire |
| 2016-11-17 | Christophe Raffalli | Practical Subtyping for System F |
| 2016-11-03 | John Gowers | Transfinite games and the sequoidal exponential |
| 2016-10-20 | Titouan Carette | Effectuses, land of probabilities |
| 2016-10-06 | André Joyal | Aspects of 2-algebras: operads, bimodules and analytic functors |
| 2016-09-29 | Fabio Pasquali | On some toposes of topological setoids |
| 2016-09-15 | Thomas Streicher | Classical realizability from relative realizability |
| 2016-07-07 | Samuel Mimram | Homological computations for term rewriting systems |
| 2016-06-30 | Pierre Clairambault | Une sémantique des jeux parallèle pour PCF |
| 2016-06-02 | Guillaume Geoffroy | Modèles de réalisabilité classique par réalisateurs universels |
| 2016-05-26 | Giulio Guerrieri | An untyped lambda-calculus generalizing Call-By-Name and Call-By-Value |
| 2016-04-26 | Gilles Dowek | Expressing theories in the λΠ-calculus modulo theory and in the Dedukti system |
| 2016-04-21 | Lionel Vaux | β-réduction et développement de Taylor |
| 2016-03-31 | Lionel Vaux | β-réduction et développement de Taylor |
| 2016-03-24 | Flavien Breuvart | From hard work to trickery: a systematic approach of probabilistic rewriting |
| 2016-03-17 | Myriam Quatrini | Caractérisation des comportements de la Ludique |
| 2016-03-03 | Hugo Herbelin | dPAω: a dependently-typed classical arithmetic in finite types which proves dependent choices |
| 2016-02-25 | Giulio Guerrieri | Open Call-by-Value |
| 2016-02-04 | Benjamin Monmege | Logics for Weighted Automata and Transducers |
| 2016-01-28 | Lionel Rieg | Vers un compilateur prouvé d'Esterel vers les circuits |
| 2016-01-21 | Matteo Acclavio | Diagrammes de cordes pour la représentation des réseaux de preuves |
| 2016-01-07 | Daniel de Carvalho | Le modèle relationnel est injectif pour MELL |
| 2015-12-10 | Luigi Santocanale | Fixed-point elimination in the Intuitionisitic Propositional Calculus |
| 2015-12-10 | Valentin Blot | Typed realizability for first-order classical analysis |
| 2015-11-26 | Yves Guiraud | Réécriture linéaire et théorème de Squier pour les algèbres |
| 2015-11-12 | Andrea Gagna | Quillen's theorem A and categories as model for homotopy types |
| 2015-10-15 | Colin Riba | Fibrations of Tree Automata |
| 2015-10-08 | Eric Hoffbeck | Utilisation de catégories supérieures pour les résolutions d'algèbres |
| 2015-09-24 | Guillaume Geoffroy | L'instruction fork et le principe d'induction en réalisabilité classique |
| 2015-07-09 | Yves Lafont | Calcul oriental |
| 2015-07-02 | Etienne Miquey | Realizability games for the specification problem |
| 2015-06-25 | Thomas Leventis | Un résultat de full-abstraction pour les arbres de Böhm du lambda-calcul probabiliste |
| 2015-06-18 | Fabio Zanasi | Interacting Hopf algebras: the string diagrammatic theory of linear subspaces |
| 2015-06-04 | Emmanuel Beffara | Vers l'unification des systèmes de types pour processus mobiles |
| 2015-05-28 | Olivier Laurent | Treillis et extensions de la logique linéaire additive |
| 2015-04-23 | Pierre Hyvernat | Représentation des fonctions continues entre "streams" (& Co.) par des types de données |
| 2015-03-26 | Jean-Louis Krivine | Bar recursion, sémantique dénotationnelle et réalisabilité classique |
| 2015-03-19 | Thomas Ehrhard | Types inductifs stricts et paresseux, du point de vue de la logique linéaire |
| 2015-02-19 | Charles Grellois | A semantic study of higher-order model-checking |
| 2015-01-29 | Michele Basaldella | Unary second-order propositional logic |
| 2015-01-08 | Marie Kerjean | Topologies faibles et logique linéaire |
| 2014-12-15 | Jean-Baptiste Midez | Une étude combinatoire du lambda-calcul avec ressources uniforme |
| 2014-10-09 | Dimitri Ara | Théorie homotopique des n-catégories |
| 2014-10-02 | Dimitri Ara | Théorie homotopique des n-catégories |
| 2014-06-12 | Clément Aubert | Programmation logique, unification et espace logarithmique |
| 2014-04-25 | Laurent Poinsot | Sur le groupoïde de géométrie d'une variété équationnelle équilibrée |
| 2014-04-18 | Marc Lasson | Canonicity of groupoids laws using parametricity theory |
| 2014-04-18 | Philip Scott | Coordinatizing MV algebras and AF C*-algebras by inverse monoids |
| 2014-04-09 | Alejandro Díaz-Caro | Type theory modulo isomorphisms |
| 2014-03-28 | Benoît Valiron | Finite Vector Spaces as Model of Simply-Typed Lambda-Calculi |
| 2014-03-18 | Benedikt Ahrens | Category theory in the Univalent Foundations |
| 2014-02-10 | Giuseppe Greco | Proof theory for dynamic logics |
| 2014-02-06 | Paolo Pistone | Une analyse philosophique et quelques résultats sur le typage |
| 2014-01-30 | Pierre Boudes | Espaces cohérents dans un cadre quantitatif |
| 2014-01-23 | Jean-Baptiste Midez | La réduction dans le λ-calcul avec ressources |
| 2014-01-16 | Alberto Carraro | Semantical analysis of λ-calculus by (Differential) Linear Logic |
| 2013-10-10 | Lionel Rieg | L'interprétation calculatoire du forcing en réalisabilité classique: l'exemple des arbres de Herbrand |
