| Your time | Speaker | Title | |
| Thu | Sep 07 | 17:00 | Leonardo de Moura | Lean 4: Empowering the Formal Mathematics Revolution and Beyond | |
| Thu | Aug 31 | 17:00 | Nat Shankar | Abstraction Engineering with the Prototype Verification System (PVS) | |
| Thu | Aug 24 | 17:00 | Urs Schreiber | Quantum Programming via Linear Homotopy Types | |
| Thu | Jun 29 | 17:00 | Nathaniel Osgood | Towards Compositional System Dynamics for Public Health | |
| Thu | Jun 22 | 17:00 | Jared Culbertson | Applying Categorical Thinking to Practical Domains | |
| Thu | Jun 15 | 17:00 | Taco Cohen | Categorical Causality & Systems Theory | |
| Thu | Jun 08 | 17:00 | Tom Hirschowitz | Abstraction in programming language theory: Howe's method | |
| Thu | Jun 01 | 17:00 | Alex Martsinkovsky | How to interpret cotorsion | |
| Thu | May 25 | 17:00 | Elaine Landry | As If Category Theory were a Foundation | |
| Thu | May 18 | 17:00 | Clark Barrett | Proof Certificates in Satisfiability Modulo Theories | |
| Thu | May 11 | 17:00 | Chad Giusti | Toward a useful category for persistent homology | |
| Thu | May 04 | 17:00 | Michael Barany | How Categories Come to Matter: On the history and sociology of categories in modern mathematics | |
| Thu | Apr 27 | 17:00 | Georges Gonthier | Foothills and cathedrals: organising the libraries behind big proofs | |
| Thu | Apr 20 | 17:00 | Davide Trotta | Generalized existential completions and applications | |
| Thu | Apr 13 | 17:00 | Urs Schreiber | Effective Quantum Certification via Linear Homotopy Types | |
| Thu | Mar 30 | 17:00 | Simon Willerton | Metric spaces, entropic spaces and convexity | |
| Thu | Mar 23 | 17:00 | Christina Vasilakopoulou | Dual algebraic structures and enrichment | |
| Thu | Mar 16 | 17:00 | Riehl, Bradley, Cheng, Dancstep, and Lugg | Category theory outreach panel | |
| Thu | Mar 09 | 17:00 | David Corfield | Philosophical perspectives on category theory | |
| Thu | Mar 02 | 17:00 | Justin Curry | Algebraic and Geometric Models for Space Networking | |
| Thu | Feb 16 | 17:00 | Sergey Goncharov | Towards a Higher-Order Mathematical Operational Semantics | |
| Thu | Feb 09 | 17:00 | Prakash Panangaden | Nuclear ideals in monoidal *-categories | |
| Thu | Feb 02 | 17:00 | Paige North | Fuzzy type theory | |
| Thu | Dec 15 | 17:00 | Andrei Rodin | Univalent Foundations and Applied Mathematics | |
| Thu | Dec 08 | 17:00 | Alexandre Miquel | Implicative algebras: a new foundation for realizability and forcing | |
| Thu | Dec 01 | 17:00 | Pawel Sobocinski | Electrical circuits with string diagrams | |
| Thu | Nov 10 | 17:00 | Gilles Dowek | From the Universality of Mathematical Truth to the Interoperability of Proof Systems | |
| Thu | Nov 03 | 17:00 | Bryce Clarke | A double-categorical approach to lenses via algebraic weak factorisation systems | |
| Thu | Oct 27 | 16:00 | Richard Zanibbi | Mathematical Information Retrieval: Searching with Formulas and Text | |
| Thu | Oct 20 | 17:00 | Robin Cockett | Turing categories | |
| Thu | Oct 13 | 17:00 | Dan Koditschek | Working Compositions for Correct Execution of Robot Task Specifications | |
| Thu | Oct 06 | 17:00 | Angeliki Koutsoukou Argyraki | The new era of formalised mathematics and the ALEXANDRIA Project | |
| Thu | Sep 29 | 17:00 | Johan Commelin | Breaking the one-mind-barrier in mathematics using formal verification | |
| Thu | Sep 22 | 17:00 | Jacques Carette | What I learned from formalizing Category Theory in Agda | |
| Thu | Sep 15 | 17:00 | Eduardo Dubuc | On localizations via homotopies | |
| Thu | Sep 08 | 17:00 | David Jaz Myers | A synthetic approach to orbifolds | |
| Thu | Sep 01 | 17:00 | Chad Scherrer | Applied Measure Theory for Composable Statistical Modeling | |
| Thu | Aug 25 | 17:00 | Andrea Censi | Categorification of Negative Information | |
| Thu | Jul 07 | 17:00 | Josef Urban | Combining learning and deduction over formal math corpora | |
| Thu | Jun 30 | 17:00 | Noam Zeilberger | Parsing as a lifting problem and the Chomsky-Schützenberger representation theorem | |
| Thu | Jun 23 | 17:00 | Moshe Vardi | Ethics Washing in AI | |
| Thu | Jun 16 | 17:00 | Christoph Benzmueller | Logico-pluralistic exploration of foundational theories with computers | |
| Thu | Jun 09 | 17:00 | Nicolas Behr | Fundamentals of Compositional Rewriting Theory | |
| Thu | Jun 02 | 17:00 | Thierry Coquand | Sheaf Cohomology in Univalent Type Theory | |
| Thu | May 26 | 17:00 | Tai-Danae Bradley | Entropy as an Operad Derivation | |
| Thu | May 19 | 17:00 | Alexandra Silva | Learning Weighted Automata over Principal Ideal Domains | |
| Thu | May 12 | 17:00 | Andrej Bauer | The countable reals | |
| Thu | May 05 | 17:00 | John Terilla | Rethinking language | |
| Thu | Apr 28 | 17:00 | Martín Escardó | Compact totally separated types in constructive univalent type theory | |
| Thu | Apr 14 | 17:00 | Leo McElroy | Making Microworlds: A Framework for Making Sense by Making Things | |
| Thu | Apr 07 | 17:00 | Giuseppe Rosolini | When an elementary quotient completion is a quasitopos | |
| Thu | Mar 31 | 17:00 | Maaike Zwart | Lessons from failing distributive laws | |
| Thu | Mar 24 | 20:00 | Dominic Verity | Zen and the art of ∞-categories | |
| Thu | Mar 17 | 17:00 | Zoé Christoff | The logic of social influence in networks | |
| Thu | Mar 03 | 17:00 | Glynn Winskel | Making concurrency functional | |
| Thu | Feb 24 | 17:00 | Bob Coecke | Compositional Intelligence | |
| Thu | Feb 17 | 17:00 | David Danks | Ethics in AI, not Ethics of AI | |
| Thu | Dec 09 | 17:00 | Robert Harper | Phase Distinctions in Type Theory | |
| Thu | Dec 02 | 17:00 | Evan Patterson | Categories of diagrams in data migration and computational physics | |
| Thu | Nov 18 | 17:00 | Paolo Perrone | The rise of quantitative category theory | |
| Thu | Nov 04 | 18:00 | Jeremy Avigad | Formal mathematics, dependent type theory, and the Topos Institute | |
| Thu | Oct 28 | 17:00 | Dorette Pronk | Doubly Lax Colimit of Double Categories with Applications | |
| Thu | Oct 21 | 17:00 | Chris Kapulkin | Cubical setting for Discrete Homotopy Theory | |
| Thu | Oct 14 | 17:00 | Andreas Blass | A topos view of axioms of choice for finite sets | |
| Thu | Oct 07 | 15:00 | Anders Mortberg | Cubical Methods in Homotopy Type Theory and Univalent Foundations | |
| Thu | Sep 30 | 15:00 | Pawel Sobocinski | Algebraic theories with string diagrams | |
| Thu | Sep 23 | 17:00 | Andrew J. Blumberg | Abstract homotopy theory for topological data analysis | |
| Thu | Sep 16 | 17:00 | Jamie Vicary | Understanding free infinity-categories | |
| Thu | Sep 09 | 17:00 | John Bourke | Tensor products, multimaps and internal homs | |
| Thu | Sep 02 | 17:00 | Florian Rabe | MMT: A UniFormal Approach to Knowledge Representation | |
| Thu | Aug 26 | 17:00 | Conor McBride | Cats and Types: Best Friends? | |
| Thu | Aug 19 | 17:00 | Valeria de Paiva | Categorical Explicit Substitutions | |
| Thu | Aug 12 | 17:00 | Kevin Buzzard | What is the point of Lean's maths library? | |
| Thu | Aug 05 | 17:00 | Todd Trimble | From 2-rigs to lambda-rings | |
| Thu | Jul 29 | 22:00 | Marcy Robertson | Topological Inspiration for Infinity Modular Operads | |
| Thu | Jul 22 | 17:00 | Walter P Tholen | What is monoidal topology? | |
| Thu | Jul 08 | 17:00 | Geoffrey Cruttwell | Categorical differential structures and their role in abstract machine learning | |
| Thu | Jul 01 | 17:00 | Lawrence Paulson | Formalising Contemporary Mathematics in Simple Type Theory | |
| Thu | Jun 24 | 18:00 | Kathryn Hess | From comonads to calculus | |
| Thu | Jun 17 | 17:00 | Chris Heunen | Sheaf representation of monoidal categories | |
| Thu | Jun 10 | 17:00 | Eugene Lerman | A category of hybrid systems | |
| Thu | Jun 03 | 17:00 | Steve Awodey | Model Structures from Models of HoTT | |
| Thu | May 27 | 17:00 | Michael Shulman | Two-dimensional semantics of homotopy type theory | |
| Thu | May 20 | 17:00 | Tobias Fritz | The law of large numbers in categorical probability | |
| Thu | May 13 | 17:00 | Maria Emilia Maietti | Quotient completions for topos-like structures | |
| Thu | May 06 | 17:00 | Emily Riehl | Contractibility as uniqueness | |
| Thu | Apr 29 | 17:00 | Jonathan Gorard | Fast Diagrammatic Reasoning and Compositional Approaches to Fundamental Physics | |
| Thu | Apr 22 | 17:00 | Shaowei Lin | Proofs as programs: challenges and strategies for program synthesis | |
| Thu | Apr 15 | 17:00 | Asgar Jamneshan | Topos theory and measurability | |
| Thu | Apr 08 | 17:00 | Joachim Kock | Noncrossing hyperchords and free probability | |
| Thu | Apr 01 | 17:00 | Dan Christensen | Reasoning in an ∞-topos with homotopy type theory | |
| Thu | Mar 25 | 18:00 | John Baez | Mathematics in the 21st century | |
| Thu | Mar 11 | 17:00 | Samson Abramsky | The logic of contextuality | |
| Thu | Feb 18 | 17:00 | Gunnar E. Carlsson | Relative topology, motion planning, and coverage problems | |
| Thu | Feb 11 | 21:00 | Richard Garner | Comodels of an algebraic theory | |
| Thu | Feb 04 | 17:00 | David Spivak | Poly: a category of remarkable abundance | |
