Topos Colloquium

Thursdays, 17:00 UTC — Online

A weekly expository talk series showcasing work towards the Topos mission, held online and live-streamed.

About

The Topos Institute Colloquium is an expository virtual talk series on topics relevant to the Topos mission and community. We usually meet over Zoom on Thursdays at 17:00 UTC. Talks are recorded, and remain available on our YouTube channel.

If you wish to be subscribed to the mailing list for weekly talk announcements, send a blank email to seminars+subscribe@topos.institute. For any queries about the colloquium, contact david+colloquium@topos.institute.

Upcoming talks

Events shown in time zone:

Themes

The colloquium centres around following four themes, with many talks fitting multiple themes.

Ethics and societal impact of mathematics and computer science

Topos aims to shape technology for public benefit via creating and deploying a new mathematical systems science. What does this mean, and how do we do it? How does technology shape people’s lives today? What are the risks that future technologies may bring? What is the role of mathematicians and computer scientists in shaping how their work has been deployed? What lessons can we learn from the past and present about successes and failures? This theme aims to spark discussion among mathematicians and computer scientists about these questions, and bring them into contact with experts on these subjects.
Applied category theory

Thinking clearly about today’s most pressing scientific, technical, and societal questions requires finding the right abstractions. Category theory can help with this by offering design principles for structuring how we account for phenomena in a specific domain, as well as how we translate problems and solutions between different domains. This theme aims to highlight recent developments in applied category theory, in domains such as computation, neuroscience, physics, artificial intelligence, game theory, and robotics.
Foundation models: Logic, categories, and type theory

Like many parts of pure mathematics, results that are initially seen as purely theoretical may not be ripe for application until much later. At Topos we foster the entire pipeline, from the creation of elegant theory to the development of its effective application. The goal of this theme is to foster the pure side of this pipeline, to take in the most beautiful results in category theory, logic, type theory, and related fields, as well as to scout for not-yet-categorical work that appears ripe for “categorification”.
Technologies and tools

Beyond its intrinsic interest, the purpose of applied mathematics is to provide a foundation for new capabilities and technologies that benefit the public. In this theme, we highlight work, at the intersection of research and engineering, that transfers ideas from applied category theory and other parts of mathematics into viable technologies, with an emphasis on software systems and tools. Topics may include scientific modeling, functional programming, differential programming, probabilistic programming, quantum computing, formal verification, and software and systems engineering.

Previous talks

Hybrid systems as coalgebras: Lyapunov morphisms for Zeno stability

Joe Moeller
2026-06-11

The projection formula, extranatural transformations and surface diagrams

Simon Willerton
2026-05-28

Demystifying Codensity Monads via Duality

Stefan Milius
2026-05-21

Many Logics, One Methodology — On the Virtues of LogiKEy in Computational Metaphysics and Ontology

Christoph Benzmueller
2026-05-07

Total Functional Programming, Reloaded

Jeremy Gibbons
2026-04-30

Control, Complete, Compute: Rig Categories in Quantum Computing

Chris Heunen
2026-04-23

Containers and Comodule Representations of Second-Order Functionals

Danel Ahman
2026-04-09

Classically laughable theorems

Andrej Bauer
2026-04-02

BV-Categories and Higher-Order Quantum Theory

James Hefford
2026-03-19

What is a monoid?

Paul Levy
2026-03-12

The Eckmann-Hilton argument in duoidal categories

Marcelo Aguiar
2026-03-05

Properties for the People

Benjamin Pierce
2026-02-26

Autoformalization and the future of math and science

Patrick Shafto
2026-02-19

Combinatory Completeness in Structured Multicategories

Chad Nester
2026-02-12

Designing and developing an industrial-strength programming language

Dan Ghica
2026-02-05

The category of schemes is abelian (and other obviously-false true things)

Inna Zakharevich
2026-01-29

Cospans of finite sets

John Baez
2025-12-11

Concrete syntax matters, actually

Slim Lim
2025-12-04

Commutative rings, bispans, and their equivariant analogues

Rune Haugseng
2025-11-06

Two-dimensional Kripke Semantics

Alex Kavvos
2025-11-06

What's up with AI?

Terry Winograd
2025-10-30

Symmetry beyond group and its description by braided fusion category

Xiao-Gang Wen
2025-10-23

Syntax and semantics for mechanical processes

Cole Comfort
2025-10-16

Behavioural Metrics via Functor Lifting – A Coalgebraic Approach

Barbara König
2025-10-09

Instances of models of double theories

Kevin Carlson
2025-10-02

A double category of transducers

Fosco Loregian
2025-09-25

Double categorical equivalences

Maru Sarazola
2025-09-18

Dependetopes and Higher Generalized Algebraic Theories

Eric Finster
2025-09-11

Towards a mathematical theory of intentional systems

Nathaniel Virgo
2025-09-04

CAP — a categorical (re)organization of computer algebra

Mohamed Barakat
2025-07-17

Abstractions for Real People

Brendan Fong
2025-07-10

ZX Calculus and Fault-tolerant quantum computing

Aleks Kissinger
2025-07-03

Opetopic shapes, combinatorially

Pierre-Louis Curien
2025-06-26

Articulating the Structure of Reasons: Logical Expressivism and Implication-Space Semantics

Robert Brandom
2025-06-19

Cartesian Fermat Categories, a new class of Cartesian Differential Categories

Jean-Simon Lemay
2025-06-12

Organisation of the Information Flow in the Perception-Action Loop

Daniel Polani
2025-05-29

Random Variables, Independence Structures and Dagger Categories of Relations

Dario Stein
2025-05-22

Duality for complete atomic partial Boolean algebras

Samson Abramsky
2025-05-15

Combinatorial foundation for planar string diagrams

Amar Hadzihasanovic
2025-05-08

Distillation systems as models of homotopy colimits

Kristine Bauer
2025-05-01

V-graded categories as a setting for enrichment and actions of monoidal categories V

Rory Lucyshyn-Wright
2025-04-24

Update rules of Pearl and Jeffrey

Bart Jacobs
2025-04-17

Beyond Tech Solutionism: Challenges of unlocking under-served community knowledge

Kate Fleming
2025-04-10

A (virtual) double category theorist's perspective on polynomials

Nathanael Arkor
2025-04-03

Geometric principles of data visualization

Juergen Jöst
2025-03-27

Language, Technology, & Care

B. Scot Rousse
2025-03-20

(Co)algebraic analysis of social systems: from graphs to hypergraphs

Nina Otter
2025-03-13

Representable Behaviour in Double Categorical Systems Theory

Matteo Capucci
2025-03-06

A categorical approach to Lyapunov stability

Joe Moeller
2025-02-27

Tensor Species: The Theory and Practice of Neural Networks

Andrew Dudzik
2025-02-13

The rabbit calculus: convolution products on double categories and categorification of rule algebra

Paul-Andre Mellies
2025-02-06

Kleisli constructions for pseudomonads

Adrian Miranda
2025-01-31

Engineering practice and the potential role of CT in systems engineering

Eswaran Subrahmanian
2024-12-12

Collective grassroots knowledge generation with lab discourse graphs

Matthew Akamatsu
2024-12-05

Unravelling the "Unreasonable Effectiveness" of Mathematics

Arezoo Islami
2024-11-14

Graphical Methods in Quantum Cryptography

Carl Miller
2024-11-07

Partial Markov Categories

Mario Román
2024-10-31

Compact Proofs: Measuring Quality of Understanding with a Compression-Based Metric

Jason Gross
2024-10-24

Quantitative results for stochastic processes

Thomas Powell
2024-10-16

Cubical types for the working formalizer

Amélia Liao
2024-10-03

Online communities as model systems for commons governance

Seth Frey
2024-09-26

What is the Identity operator?

Chris Fields
2024-09-19

Semantics for Reactive Probabilistic Programming

Christine Tasson
2024-09-12

Polynomial Interfaces

Spencer Breiner
2024-09-05

Totally Live Programming and Proving in Hazel

Cyrus Omar
2024-08-29

How to Make Mathematicians Into Programmers (And Vice Versa)

Will Chrichton
2024-08-22

The Automation of Mathematics from an Anthropological Perspective

Rodrigo Ochigame
2024-08-15

A generalization of inversion using Bayes' rule with applications to quantum

Arthur J Parzygnat
2024-08-08

On Taming Differentiable Logics

Kathrin Stark
2024-08-01

From gs-monoidal to cartesian categories: a structural analysis

Fabio Gadducci
2024-07-11

Topological Data Analysis of Spatial Systems

Mason Porter
2024-06-27

Parametric Profunctor Preoptics

Bartosz Milewski
2024-06-13

Three toposes for probability and randomness

Alex Simpson
2024-06-06

The Fundamental Theorem of Calculus: point-free

Steve Vickers
2024-05-30

Point-free topology is known in various guises (locales, formal topology), but can be boiled down to a procedure of defining the points of a space not (“point-set”) as elements of a set, but as models of a logical theory. This is for a constrained “geometric” logic, so that the opens of the space correspond to propositional formulae derived from the theory: thus the theory defines both the points and the topology. Then continuity of maps just means that they are constructed in accordance with the constraints of the logic.

Why bother to do topology that way? After all, the logic is even more constrained than constructive reasoning, and we still don’t know how far it reaches.

The first reason is that it quite painlessly extends to toposes, viewed as generalized spaces. This uses the machinery of classifying toposes, but only in an unobtrusive way [1]. Many proper classes can then be viewed as point-free spaces - just write down a geometric theory whose models are the elements of the class.

The second reason follows from the first but can then be applied back to ungeneralized spaces in a very natural treatment of bundles. Theory presentations can themselves be described as the models of a geometric theory, and this allows us to view bundles as continuously mapping base points to spaces (the fibres). For physics in particular, this invites exploration of how much can be done using geometric methods. See eg [2].

Meanwhile, there is the question of how much ordinary mathematics, and in particular real analysis, can be done in this style. I present as a case study the Fundamental Theorem of Calculus [3]. This illustrates some typically geometric features of the reasoning, such as attention paid to one-sided reals and the use of hyperspaces and their analogues, and some exploitation of the geometric fact that everything is continuous, as well as a cute new trick using uniform probability measures.

Steven Vickers “Topical categories of domains”, Mathematical Structures in Computer Science 9 (1999)
Bas Spitters, Steven Vickers and Sander Wolters “Gelfand spectra in Grothendieck toposes using geometric mathematics”, Electronic Proceedings in Theoretical Computer Science 158 (2014)
Steven Vickers “The Fundamental Theorem of Calculus point-free, with applications to exponentials and logarithms”, arXiv:2312.05228

Monoidal bicategories, differential linear logic, and analytic functors

Nicola Gambino
2024-05-23

Effectful trace semantics via effectful streams

Elena Di Lavore
2024-05-16

Categories of Classes for Collection Monads

Eugenio Moggi
2024-05-09

Diagrammatic Algebra of First Order Logic

Filippo Bonchi
2024-05-02

Co-Design of Complex Systems: From Autonomy to Future Mobility

Gioele Zardini
2024-04-25

Certainty or Intelligence: Pick One!

Edward Lee
2024-04-18

Uniting Game Theory, Math Stars, and Actors To Build Human Intelligence in the AI Age

Po-Shen Loh
2024-04-04

Sociotechnical infrastructure for mathematics research

Steven Clontz
2024-03-28

Polynomial functors — from elementary arithmetic to infinity-operads

Joachim Kock
2024-02-22

Free bicompletion of categories revisited (part 1)

André Joyal
2024-02-15

Cauchy Completeness and Adjoints in Double Categories

Susan Niefield
2024-02-08

Cohomological aspects of information

Juan Pablo Vigneaux
2024-01-25

Aspects of a Mathematical Theory of Data

John Cartmell
2024-01-18

The functorial difference operator

Robert Paré
2024-01-11

Higher topos theory and Goodwillie Calculus

André Joyal
2023-12-14

Models for (∞,n)-categories with discreteness conditions

Julie Bergner
2023-12-07

Who Owns Mathematics: A Question of Identity

Minhyong Kim
2023-11-30

Normalising ethical reasoning for mathematicians

Maurice Chiodo
2023-11-16

(Higher) category theory in Cat^#

Brandon Shapiro
2023-11-02

Entropy and diversity: the axiomatic approach

Tom Leinster
2023-10-26

Simplicial delta versus fat delta in higher category theory

Simona Paoli
2023-10-19

Programming for the Planet

Dominic Orchard
2023-10-12

Synthetic Domains in the 21st Century

Jonathan Sterling
2023-09-28

It is easy to teach a student how to give a naïve denotational semantics to a typed lambda calculus without recursion, and then use it to reason about the equational theory: a type might as well be a set, and a program might as well be a function, and equational adequacy at base type is established using a logical relation between the initial model and the category of sets. Adding any non-trivial feature to this language (e.g. general recursion, polymorphism, state, etc.) immediately increases the difficulty beyond the facility of a beginner: to add recursion, one must replace sets and functions with domains and continuous maps, and to accommodate polymorphism and state, one must pass to increasingly inaccessible variations on this basic picture.

The dream of the 1990s was to find a category that behaves like SET in which even general recursive and effectful programming languages could be given naïve denotational semantics, where types are interpreted as “sets” and programs are interpreted as a “functions”, without needing to check any arduous technical conditions like continuity. The benefit of this synthetic domain theory is not only that it looks “easy” for beginners, as more expert-level constructions like powerdomains or even domain equations for recursively defined semantic worlds become simple and direct. Although there have been starts and stops, the dream of synthetic domain theory is alive and well in the 21st Century. Today’s synthetic domain theory is, however, both more modular and more powerful than ever before, and has yielded significant results in programming language semantics including simple denotational semantics for an state of the art programming language with higher-order polymorphism, dependent types, recursive types, general reference types, and first-class module packages that can be stored in the heap.

In this talk, I will explain some important classical results in synthetic domain theory as well as more recent results that illustrate the potential impact of “naïve denotational semantics” on the life of a workaday computer scientist.

Emergent Selves and Unconventional Intelligences: where philosophy and engineering meet

Michael Levin
2023-09-21

Lean 4: Empowering the Formal Mathematics Revolution and Beyond

Leonardo de Moura
2023-09-07

Abstraction Engineering with the Prototype Verification System (PVS)

Nat Shankar
2023-08-31

Logic has always played a central role in computing. One successful application of logic is its use in specifying and modeling computational behavior, and in proving properties of computation systems. SRI’s PVS was released thirty years ago with the goal of democratizing interactive theorem proving by combining an expressive formalism with powerful automated reasoning tools for building and maintaining complex formalizations and proofs. We describe some of the features of PVS for defining and reasoning with mathematical abstractions and bridging the gap between informal and formalized mathematical discourse. PVS features an expressive-order logic with algebraic/coalgebraic datatypes, dependent predicate subtypes, and parametric theories. The interactive theorem prover employs a range of automated proof strategies for simplification, rewriting, and case analysis, along with built-in decision procedures for SAT and SMT solving. The applicative fragment of PVS can be viewed as a functional programming language, and efficient executable code can be generated in Common Lisp and C, among other languages. PVS includes extensive libraries spanning a range of topics in mathematics and computing. The talk is an informal overview of the underlying theoretical foundations, and the proof and code generation capabilities of PVS.

Bio: Dr. Natarajan Shankar is a Distinguished Senior Scientist and SRI Fellow at the SRI Computer Science Laboratory. He received a B.Tech. degree in Electrical Engineering from the Indian Institute of Technology, Madras, and Ph.D. in Computer Science from the University of Texas at Austin. He is the author of the book, “Metamathematics, Machines, and Godel’s Proof”, published by Cambridge University Press. Dr. Shankar is the co-developer of a number of technologies including the PVS interactive proof assistant, the SAL model checker, the Yices SMT solver, and the Arsenal semantic parser. He is a co-recipient of the 2012 CAV Award and the recipient of the 2022 Herbrand Award.

Quantum Programming via Linear Homotopy Types

Urs Schreiber
2023-08-24

The intricacies of realistic — namely: of classically controlled and (topologically) error-protected — quantum algorithms arguably make computer-assisted verification a practical necessity; and yet a satisfactory theory of dependent quantum data types had been missing, certainly one that would be aware of topological error-protection.

To solve this problem we present Linear homotopy type theory (LHoTT) as a programming and certification language for quantum computers with classical control and topologically protected quantum gates, focusing on (1.) its categorical semantics, which is a homotopy-theoretic extension of that of Proto-Quipper and a parameterized extension of Abramsky et al.’s quantum protocols, (2.) its expression of quantum measurement as a computational effect induced from dependent linear type formation and reminiscent of Lee at al.‘s dynamic lifting monad but recovering the interacting systems of Coecke et al.‘s “classical structures” monads.

Namely, we have recently shown that classical dependent type theory in its novel but mature full-blown form of Homotopy Type Theory (HoTT) is naturally a certification language for realistic topological logic gates. But given that categorical semantics of HoTT is famously provided by parameterized homotopy theory, we had argued earlier [Sc14] for a quantum enhancement LHoTT of classical HoTT, now with semantics in parameterized stable homotopy theory. This linear homotopy type theory LHoTT has meanwhile been formally described; here we explain it as the previously missing certified quantum language with monadic dynamic lifting, as announced in.

Concretely, we observe that besides its support, inherited from HoTT, for topological logic gates, LHoTT intrinsically provides a system of monadic computational effects which realize what in algebraic topology is known as the ambidextrous form of Grothendieck’s “Motivic Yoga”; and we show how this naturally serves to code quantum circuits subject to classical control implemented via computational effects. Logically this emerges as a linearly-typed quantum version of epistemic modal logic inside LHoTT, which besides providing a philosophically satisfactory formulation of quantum measurement, makes the language validate the quantum programming language axioms proposed by Staton; notably the deferred measurement principle is verified by LHoTT.

Finally we indicate the syntax of a domain-specific programming language QS (an abbreviation both for “Quantum Systems” and for “QS^0 -modules” aka spectra) which sugars LHoTT to a practical quantum programming language with all these features; and we showcase QS-pseudocode for simple forms of key algorithm classes, such as quantum teleportation, quantum error-correction and repeat-until-success quantum gates.

(This is joint work with D. J. Myers, M. Riley and H. Sati.)

Towards Compositional System Dynamics for Public Health

Nathaniel Osgood
2023-06-29

For decades, System Dynamics (SD) modeling has served as a prominent, diagram-centric methodology used for public health modeling. Much of its strength arises from its versatile use of 3 types of diagrams, with each serving both to elevate transparency across the interdisciplinary teams responsible for most impactful models, and to reason about patterns of system behavior. Causal loop diagrams (CLDs) are used in semi-qualitative processes early in the modeling process and seek to support insight into feedback structure, behavioral modes, and leverage points. As modeling proceeds, system structure diagrams further distinguish stocks (accumulations) from flows and material from informational dependencies. Stock & flow diagrams build on that representation to characterize mathematical dependencies, quantify parameters and initial values for stocks, and have been particularly widely used in scenario simulation in public health and mathematical epidemiology. While ubiquitous use of diagrams renders SD modeling markedly effective in supporting team science and shaping stakeholders’ mental models, existing tools suffer from a number of shortcomings. These include poor support for modularity, cumbersome and obscurant model stratification, and an inability to capture the relationships between the 3 diagram types. Within this talk, we describe initial progress towards creating a framework for compositional System Dynamics, including theory, API support via StockFlow.jl within AlgebraicJulia, and ModelCollab – a real-time collaborative tool to support interdisciplinary teams in modularly building, composing and flexibly analyzing Stock & Flow diagrams. Our approach separates syntax from semantics, and characterizes diagrams using copresheaves with a schema category. Diagram composition draws on the theory of structured cospans and undirected wiring diagrams, and employs pullbacks for model stratification. Model interpretation is achieved via functorial semantics, with ordinary differential equations being just one of several semantic domains supported. After describing the current state of implementation, we describe plans for future work, including enriching support for CLDs, and adding support for several computational statistics algorithms and additional types of structurally-informed model analyses. This is joint work with John Baez, Evan Patterson, Nicholas Meadows, Sophie Libkind, Alex Alegre and Eric Redekopp.

Applying Categorical Thinking to Practical Domains

Jared Culbertson
2023-06-22

Categorical Causality & Systems Theory

Taco Cohen
2023-06-15

Abstraction in programming language theory: Howe's method

Tom Hirschowitz
2023-06-08

How to interpret cotorsion

Alex Martsinkovsky
2023-06-01

As If Category Theory were a Foundation

Elaine Landry
2023-05-25

Proof Certificates in Satisfiability Modulo Theories

Clark Barrett
2023-05-18

Toward a useful category for persistent homology

Chad Giusti
2023-05-11

How Categories Come to Matter: On the history and sociology of categories in modern mathematics

Michael Barany
2023-05-04

Foothills and cathedrals: organising the libraries behind big proofs

Georges Gonthier
2023-04-27

Generalized existential completions and applications

Davide Trotta
2023-04-20

Effective Quantum Certification via Linear Homotopy Types

Urs Schreiber
2023-04-13

To solve this problem we present Linear homotopy type theory (LHoTT) as a programming and certification language for quantum computers with classical control and topologically protected quantum gates, focusing on (1.) its categorical semantics, which is a homotopy-theoretic extension of that of Proto-Quipper and a parameterized extension of Abramsky et al.’s quantum protocols, (2.) its expression of quantum measurement as a computational effect induced from dependent linear type formation and reminiscent of Lee at al.’s dynamic lifting monad but recovering the interacting systems of Coecke et al.’s “classical structures” monads.

(This is joint work with D. J. Myers, M. Riley and H. Sati. Slides will be available at: ncatlab.org/schreiber/show/Quantum+Certification+via+Linear+Homotopy+Types)

Metric spaces, entropic spaces and convexity

Simon Willerton
2023-03-30

Dual algebraic structures and enrichment

Christina Vasilakopoulou
2023-03-23

Category theory outreach panel

Riehl, Bradley, Cheng, Dancstep, and Lugg
2023-03-16

Philosophical perspectives on category theory

David Corfield
2023-03-09

Algebraic and Geometric Models for Space Networking

Justin Curry
2023-03-02

Towards a Higher-Order Mathematical Operational Semantics

Sergey Goncharov
2023-02-16

Nuclear ideals in monoidal *-categories

Prakash Panangaden
2023-02-09

Fuzzy type theory

Paige North
2023-02-02

Univalent Foundations and Applied Mathematics

Andrei Rodin
2022-12-15

Implicative algebras: a new foundation for realizability and forcing

Alexandre Miquel
2022-12-08

Electrical circuits with string diagrams

Pawel Sobocinski
2022-12-01

From the Universality of Mathematical Truth to the Interoperability of Proof Systems

Gilles Dowek
2022-11-10

A double-categorical approach to lenses via algebraic weak factorisation systems

Bryce Clarke
2022-11-03

Mathematical Information Retrieval: Searching with Formulas and Text

Richard Zanibbi
2022-10-27

Turing categories

Robin Cockett
2022-10-20

Working Compositions for Correct Execution of Robot Task Specifications

Dan Koditschek
2022-10-13

A long tradition in robotics has deployed dynamical primitives as empirical modules of behavior [1]. Physically grounded formalization of these practices offers the prospect of an expressive programming language of work for dynamically dexterous robotics whose programs lead to task and motion planners with associated controllers that are correct by design [2]. This talk will offer a brief progress report on a bottom-up robotics research agenda seeking to formalize the use of Lagrangian energy landscapes as “letters” whose hierarchical [3], parallel [4] and sequential [5] compositions yield “words” of hybrid dynamical systems with guaranteed behavioral properties. Attention then shifts to an emerging architecture for top-down task and motion planning [6] that offers the promise of abstract, semantic, formal specification [7] for mobile manipulation tasks carried out by general purpose robots [8] in learned, geometrically complicated environments [9].

The talk concludes with a more speculative appraisal of the prospects for a unified programming environment allowing the expressive top-down specification of robot behavior with automatic compilation into bottom-up words of work that are correct by design. A recent categorical treatment [10] of robot hybrid dynamical systems [11] encodes a well-grounded version of sequential composition [12] and a weak but still practicable version of hierarchical composition [3], while neglecting the consideration of cross-talk [4] in its idealization of parallel composition as a monoidal product. Subsequent results imbue a slightly restricted version of this hybrid dynamical category [10] with a version of Conley’s fundamental theorem [13] guaranteeing the existence of global Lyapunov functions that decompose a suitably formulated relaxation of the hybrid state space into a covering by attractor basins and their boundaries [14]. Thus equipped with generalized energy landscapes, more physically grounded refinements of this hybrid dynamical category may yield a practicable type theory whose associated resource-aware linear logic clauses might be integrated into the more expressive linear temporal logic interface to the task and motion planning architecture of [7]. Such future developments would greatly advance the longer term agenda toward an empirically practicable theory of “programming work” [2].

M. H. Raibert, Legged Robots That Balance. Cambridge: MIT Press, 1986.
D. E. Koditschek, “What Is Robotics? Why Do We Need It and How Can We Get It?,” Annu. Rev. Control Robot. Auton. Syst., vol. 4, no. 1, pp. 1–33, May 2021, doi: 10.1146/annurev-control-080320-011601.
R. J. Full and D. E. Koditschek, “Templates and anchors: neuromechanical hypotheses of legged locomotion on land,” J. Exp. Biol., vol. 202, pp. 3325–3332, 1999.
A. De, S. A. Burden, and D. E. Koditschek, “A hybrid dynamical extension of averaging and its application to the analysis of legged gait stability:,” Int. J. Robot. Res., vol. 37, no. 2–3, pp. 266–286, Mar. 2018, doi: 10.1177/0278364918756498.
R. R. Burridge, A. A. Rizzi, and D. E. Koditschek, “Toward a systems theory for the composition of dexterous robot behaviours,” Robot. Res. Seventh Int. Symp. ISRR’95, pp. 149–161.
V. Vasilopoulos et al., “Reactive Semantic Planning in Unexplored Semantic Environments Using Deep Perceptual Feedback,” IEEE Robot. Autom. Lett., vol. 5, no. 3, pp. 4455–4462, Jul. 2020, doi: 10.1109/LRA.2020.3001496.
V. Vasilopoulos, Y. Kantaros, G. Pappas, and D. Koditschek, “Reactive Planning for Mobile Manipulation Tasks in Unexplored Semantic Environments,” IEEE Int. Conf. Robot. Autom. ICRA, May 2021, [Online]. Available: https://repository.upenn.edu/ese_papers/880
T. T. Topping, V. Vasilopoulos, A. De, and D. Koditschek E., “Composition of Templates for Transitional Pedipulation Behaviors,” in Proc. Int. Symp. Rob. Res., 2019. [Online]. Available: https://repository.upenn.edu/ese_papers/860/
V. Vasilopoulos, G. Pavlakos, K. Schmeckpeper, K. Daniilidis, and D. E. Koditschek, “Reactive Navigation in Partially Familiar Non-Convex Environments Using Semantic Perceptual Feedback,” Int. J. Robot. Res., vol. 41, no. 1, pp. 85–126, Jan. 2022, doi: 10.1177/02783649211048931.
J. Culbertson, P. Gustafson, D. E. Koditschek, and P. F. Stiller, “Formal composition of hybrid systems,” Theory Appl. Categ., vol. 35, no. 45, pp. 1634–1682, Oct. 2020.
A. M. Johnson, S. A. Burden, and D. E. Koditschek, “A hybrid systems model for simple manipulation and self-manipulation systems,” Int. J. Robot. Res., vol. 35, no. 11, pp. 1354–1392, Sep. 2016, doi: 10.1177/0278364916639380.
R. R. Burridge, A. A. Rizzi, and D. E. Koditschek, “Sequential Composition of Dynamically Dexterous Robot Behaviors,” Int. J. Robot. Res., vol. 18, no. 6, pp. 534–555, 1999, doi: 10.1177/02783649922066385.
C. R. Robinson, Dynamical Systems: Stability, Symbolic Dynamics, and Chaos, Second. Boca Raton, FL: CRC Press, 1999. Accessed: Jan. 29, 2017. [Online]. Available: http://imb-biblio.u-bourgogne.fr/Record.htm?record=325212414349&idlist=1
M. D. Kvalheim, P. Gustafson, and D. E. Koditschek, “Conley’s Fundamental Theorem for a Class of Hybrid Systems,” SIAM J. Appl. Dyn. Syst., pp. 784–825, Jan. 2021, doi: 10.1137/20M1336576.

The new era of formalised mathematics and the ALEXANDRIA Project

Angeliki Koutsoukou Argyraki
2022-10-06

Breaking the one-mind-barrier in mathematics using formal verification

Johan Commelin
2022-09-29

What I learned from formalizing Category Theory in Agda

Jacques Carette
2022-09-22

On localizations via homotopies

Eduardo Dubuc
2022-09-15

A synthetic approach to orbifolds

David Jaz Myers
2022-09-08

Applied Measure Theory for Composable Statistical Modeling

Chad Scherrer
2022-09-01

Categorification of Negative Information

Andrea Censi
2022-08-25

Combining learning and deduction over formal math corpora

Josef Urban
2022-07-07

Parsing as a lifting problem and the Chomsky-Schützenberger representation theorem

Noam Zeilberger
2022-06-30

Joint work with Paul-André Melliès.

In “Functors are Type Refinement Systems” [1], we argued for the idea that rather than being modelled merely as categories, type systems should be modelled as functors p : D → T from a category D whose morphisms are typing derivations to a category T whose morphisms are the terms corresponding to the underlying subjects of those derivations. One advantage of this fibrational point of view is that the notion of typing judgment receives a simple mathematical status, as a triple (R,f,S) consisting of two objects R, S in D and a morphism f in T such that p(R)=dom(f) and p(S)=cod(f). The question of finding a typing derivation for a typing judgment (R,f,S) then reduces to the lifting problem of finding a morphism α : R → S such that p(α)=f. We developed this perspective in a series of papers, and believe that it may be usefully applied to a large variety of deductive systems, beyond type systems in the traditional sense. In this work [2], we focus on derivability in context-free grammars, a classic topic in formal language theory with wide applications in computer science.

The talk will begin by explaining how derivations in any context-free grammar G may be naturally encoded by a functor of operads p : Free S → W[Σ] from a freely generated operad into a certain “operad of spliced words”. This motivates the introduction of a more general notion of context-free grammar over any category C, defined as a finite species S equipped with a color denoting the start symbol, and a map of species φ : S → W[C] into the operad of spliced arrows in C, which induces a unique functor p : Free S → W[C] generating a context-free language of arrows in C. We will see that many standard concepts and properties of context-free grammars and languages can be formulated within this framework, thereby admitting simpler analysis, and that parsing may indeed be profitably considered from a fibrational perspective, as a lifting problem along a functor from a freely generated operad.

The second half of the talk will be devoted to a new proof of the Chomsky-Schützenberger Representation Theorem. An important ingredient is the identification of a left adjoint C[−] : Operad → Cat to the operad of spliced arrows functor W[−] : Cat → Operad. This construction builds the contour category C[O] of any operad O, whose arrows have a geometric interpretation as “oriented contours” of the operations of O. A direct consequence of the contour / splicing adjunction is that every finite species equipped with a color induces a universal context-free grammar, generating a language of tree contour words. Finally, we prove a generalization of the Chomsky-Schützenberger Representation Theorem, establishing that any context-free language of arrows over a category C is the functorial image of the intersection of a C-chromatic tree contour language and a regular language.

P.-A. Melliès and N. Zeilberger, Functors are type refinement systems, POPL 2015
P.-A. Melliès and N. Zeilberger, Parsing as a lifting problem and the Chomsky-Schützenberger representation theorem, 2022 (to appear)

Ethics Washing in AI

Moshe Vardi
2022-06-23

Logico-pluralistic exploration of foundational theories with computers

Christoph Benzmueller
2022-06-16

Fundamentals of Compositional Rewriting Theory

Nicolas Behr
2022-06-09

This presentation is based upon [1] (joint work with R. Harmer and J. Krivine).

Categorical rewriting theory is a research field in both computer science and applied category theory, with a rich history spanning over 50 years of active developments, starting with the pioneering work of Ehrig in the 1970s.

In this talk, I will present recent results [1] on a novel foundation for reasoning about rewriting theories via so-called compositional rewriting double categories (crDCs). The design principles followed in this approach are the typical “unify and conquer” strategy of applied category theory and a particular variant of the notion of compositionality.

To wit, crDCs permit to formulate a wide variety of categorical rewriting semantics uniformly, whereby the horizontal category for a given semantics models the rewriting rules, while the vertical category models matchings and co-matchings of rules into objects, and where the squares model so-called direct derivations (i.e., individual rewriting steps). Even before considering compositionality, it is already noteworthy that in order for crDCs to be well-defined, strong constraints are imposed upon the horizontal and vertical categories and the squares of the crDC, which in effect suggest categories with adhesivity properties (e.g., toposses, quasi-toposses, adhesive HLR categories,…) as natural starting points for constructing crDCs. In this sense, the notion of crDCs thus permits to justify the by now standard approach for categorical rewriting theories developed over the past 20 years as being based upon categories with adhesivity properties (starting with the seminal work of Lack and Sobocinski on adhesive categories) from a clear mathematical high-level perspective.

Compositionality, on the other hand, is a much deeper mathematical property that a categorical rewriting theory may carry. This property entails the existence of so-called Concurrency and Associativity Theorems. The former concerns being able to reason on two-step rewriting sequences via implementing the overall effect of the two-step rewrite via a composite rule applied in a single rewrite step, and vice versa. The Associativity Theorem then implies that the operation of forming compositions of rewriting rules is, in a certain sense, associative. Compositionality is a necessary and crucial ingredient in the stochastic mechanics and rule algebra formalism developed by Behr et al. since 2015, and which permits to provide a mathematically fully consistent and universal formalism for continuous- [2] and discrete-time Markov Chains [3] (central to applications of rewriting to bio- and organo-chemistry, social network modeling, etc.) and rule-algebraic combinatorics [4].

A central result of [1] is then that a sufficient set of conditions on a double category to model a compositional rewriting theory consists in requiring certain fibrational properties for the vertical source and target functors from squares of the double categories, i.e., that they are (residual) multi-opfibrations. I will sketch how these fibrational properties in conjunction with the other crDC axioms yield a completely uniform proof of both the Concurrency and the Associativity Theorems, and, time permitting, how a large variety of categorical rewriting semantics indeed fall under the umbrella of our novel crDC formalism.

Finally, I will provide an overview of open questions and potential fruitful cross-connections of crDC theory with the TIC and broader ACT communities.

N. Behr, R. Harmer and J. Krivine, “Fundamentals of Compositional Rewriting Theory”, https://arxiv.org/abs/2204.07175
N. Behr, J. Krivine, J.L. Andersen, D. Merkle (2021), “Rewriting theory for the life sciences: A unifying theory of CTMC semantics”, https://doi.org/10.1016/j.tcs.2021.07.026
N. Behr, B.S. Bello, S. Ehmes, R. Heckel (2021), “Stochastic Graph Transformation For Social Network Modeling”, https://doi.org/10.4204/EPTCS.350.3
N. Behr (2021), “On Stochastic Rewriting and Combinatorics via Rule-Algebraic Methods”, http://dx.doi.org/10.4204/EPTCS.334.2

Sheaf Cohomology in Univalent Type Theory

Thierry Coquand
2022-06-02

Entropy as an Operad Derivation

Tai-Danae Bradley
2022-05-26

Learning Weighted Automata over Principal Ideal Domains

Alexandra Silva
2022-05-19

The countable reals

Andrej Bauer
2022-05-12

Joint work with James E. Hanson from the University of Maryland.

In 1874 Georg Cantor published a theorem stating that every sequence of reals is avoided by some real, thereby showing that the reals are not countable. Cantor’s proof uses classical logic. There are constructive proofs, although they all rely on the axiom of countable choice. Can the real numbers be shown uncountable without excluded middle and without the axiom of choice? An answer has not been found so far, although not for lack of trying.

We show that there is a topos in which the real numbers are countable, i.e., there is an epimorphism from the object of natural numbers to the object of Dedekind reals. Therefore, higher-order intuitionistic logic cannot show the reals to be uncountable.

The starting point of our construction is a sequence of reals, shown to exist by Joseph S. Miller from University of Wisconsin–Madison, with a strong counter-diagonalization property: if an oracle Turing machine computes a specific real number, when given any oracle representing Miller’s sequence, then the number appears in the sequence. One gets the idea that the reals ought to be countable in a realizability topos built from Turing machines with oracles for Miller’s sequence. However, we cannot just use ordinary realizability, because all realizability toposes validate countable choice and consequently the uncountability of the reals.

To obtain a topos with countable reals, we define a variant of realizability which we call parameterized realizability. First we define parameterized partial combinatory algebras (ppca), which are partial combinatory algebras whose evaluation depends on a parameter. We then define parameterized realizability toposes. In these realizers witness logical statements uniformly in the parameters. The motivating example is the parameterized realizability topos built from the ppca of oracle Turing machines parameterized by oracles for Miller’s sequence. In this topos, Miller’s sequence is the desired epimorphism from natural numbers to Dedekind reals.

Rethinking language

John Terilla
2022-05-05

Compact totally separated types in constructive univalent type theory

Martín Escardó
2022-04-28

Making Microworlds: A Framework for Making Sense by Making Things

Leo McElroy
2022-04-14

When an elementary quotient completion is a quasitopos

Giuseppe Rosolini
2022-04-07

Lessons from failing distributive laws

Maaike Zwart
2022-03-31

Zen and the art of ∞-categories

Dominic Verity
2022-03-24

You may well have heard the rumour that ∞-category theory is “really just like category theory with a little homotopy theory thrown in”. Inspired by that comment, you might even have headed to a book on ∞-categories or to the nLab to find out more, only to find that things in the ∞-world are far from that simple.

Firstly you will have discovered that there is no universal agreement on what an ∞-category actually is. Instead, you’ve been met with a proliferation of ∞-categorical models; simplicially enriched categories, quasi-categories, (iterated) complete Segal spaces, complicial sets, Θ-spaces and so on. Then you discover, to your horror, that each one of these models supports its own particular interpretations of common categorical concepts, some of which appear far more familiar than others. Finally, you realise that the relationships between the category theories developed for each model are also much less than clear.

If this weren’t enough to leave anyone reaching for the Aspirin bottle, there is more bad news to come. It quickly becomes clear that there exists quite a large gap between the informal language used to describe ∞-categorical arguments, in blog posts and wiki articles, and the corresponding formal arguments expressed in any particular model of ∞-categories. Most of these are given either as concrete constructions with simplicial (or increasingly cubical) objects or as abstract model category theoretic arguments. Now I have no doubt that we “all” love a good simplicial argument, but encoding things in this way does very little to aid our categorical intuition.

There must be a better way!

In this talk we discuss recent developments in ∞-technology that seek to address these issues. Specifically, we review the current state of the art in model agnostic ∞-category theory [2], which seeks to provide a unified account of ∞-category theory freed from the straight jacket of a specific model. This allows both for the model independent, synthetic development of ∞-categorical results and for the transport of analytically derived such results from one model to another. We shall also see how these techniques are rapidly being reframed in type theoretic terms, through the development of directed type theory [1,3], thereby promising a more natural language for the formal development of ∞-categorical concepts and results.

E. Riehl, M. Shulman, A type theory for synthetic ∞-categories, High. Struct. 1 (2017) 147224.
E. Riehl, D. Verity, Elements of ∞-category theory, Cambridge University Press, 2022.
J. Weinberger, A synthetic perspective on (∞,1)-category theory: Fibrational and semantic aspects, arXiv Preprint arXiv:2202.13132. (2022).

The logic of social influence in networks

Zoé Christoff
2022-03-17

Making concurrency functional

Glynn Winskel
2022-03-03

Compositional Intelligence

Bob Coecke
2022-02-24

Ethics in AI, not Ethics of AI

David Danks
2022-02-17

Phase Distinctions in Type Theory

Robert Harper
2021-12-09

Categories of diagrams in data migration and computational physics

Evan Patterson
2021-12-02

The rise of quantitative category theory

Paolo Perrone
2021-11-18

Formal mathematics, dependent type theory, and the Topos Institute

Jeremy Avigad
2021-11-04

Doubly Lax Colimit of Double Categories with Applications

Dorette Pronk
2021-10-28

Cubical setting for Discrete Homotopy Theory

Chris Kapulkin
2021-10-21

A topos view of axioms of choice for finite sets

Andreas Blass
2021-10-14

Cubical Methods in Homotopy Type Theory and Univalent Foundations

Anders Mortberg
2021-10-07

Algebraic theories with string diagrams

Pawel Sobocinski
2021-09-30

Abstract homotopy theory for topological data analysis

Andrew J. Blumberg
2021-09-23

Understanding free infinity-categories

Jamie Vicary
2021-09-16

Tensor products, multimaps and internal homs

John Bourke
2021-09-09

MMT: A UniFormal Approach to Knowledge Representation

Florian Rabe
2021-09-02

Cats and Types: Best Friends?

Conor McBride
2021-08-26

Categorical Explicit Substitutions

Valeria de Paiva
2021-08-19

What is the point of Lean's maths library?

Kevin Buzzard
2021-08-12

From 2-rigs to lambda-rings

Todd Trimble
2021-08-05

Topological Inspiration for Infinity Modular Operads

Marcy Robertson
2021-07-29

What is monoidal topology?

Walter P Tholen
2021-07-22

Categorical differential structures and their role in abstract machine learning

Geoffrey Cruttwell
2021-07-08

Formalising Contemporary Mathematics in Simple Type Theory

Lawrence Paulson
2021-07-01

From comonads to calculus

Kathryn Hess
2021-06-24

Sheaf representation of monoidal categories

Chris Heunen
2021-06-17

A category of hybrid systems

Eugene Lerman
2021-06-10

Model Structures from Models of HoTT

Steve Awodey
2021-06-03

Two-dimensional semantics of homotopy type theory

Michael Shulman
2021-05-27

The law of large numbers in categorical probability

Tobias Fritz
2021-05-20

Quotient completions for topos-like structures

Maria Emilia Maietti
2021-05-13

In this talk we report fundamental results concerning free completions with quotients of specific Lawvere doctrines for building toposes, quasi-toposes and predicative versions of them. Our final goal is to use such completions for modelling foundations of constructive and classical mathematics which are predicative in the sense of Poincaré, Weyl and Feferman, including that in [M09]. We first recall how the tool of completing an elementary existential Lawvere doctrine with exact quotients is the fundamental construction behind the tripos-to-topos construction in [HJP80] beside including as instances both the exact completion of a regular category and that of a weakly lex finite product category, as reported in [MR15]. We then describe recent work with Fabio Pasquali and Pino Rosolini where we show how the elementary quotient completion of an elementary Lawvere doctrine in [MR13] is the fundamental construction behind a tripos-to-quasi-topos construction including toposes as exact completions of a left exact category in [Me03] as instances. We also mention a joint work with Davide Trotta where we extend results in [MPR17] about tripos-to-topos constructions coinciding with exact completions of a left exact category. We end by applying the elementary quotient completion to build examples of predicative toposes including the Effective Predicative Topos in [MM21].

[HJP80] J.M. Hyland, P. T. Johnstone and A.M.Pitts. Tripos theory. Math. Proc. Cambridge Philos. Soc. 88, 205-232, 1980
[M09] M.E. Maietti. A minimalist two-level foundation for constructive mathematics. Annals of Pure and Applied Logic, 160(3): 319-354, 2009
[MR13] M.E. Maietti and G. Rosolini. Elementary quotient completion. Theory and Applications of Categories, 27(17): 445–463, 2013
[MR15 ] M.E. Maietti and G. Rosolini. Unifying Exact Completions. Applied Categorical Structures 23(1): 43-52, 2015
[MPR17] M.E. Maietti, F. Pasquali and G. Rosolini. Triposes, exact completions, and Hilbert’s ε-operator. Tbilisi Mathematical Journal. 10(3): 141-66, 2017
[Me03] M. Menni. A characterization of the left exact categories whose exact completions are toposes. Journal of Pure and Applied Algebra, 3(177): 287-301, 2003
[MM21] M.E. Maietti, S. Maschio. A predicative variant of Hyland’s Effective Topos. To appear in The Journal of Symbolic Logic

Contractibility as uniqueness

Emily Riehl
2021-05-06

Fast Diagrammatic Reasoning and Compositional Approaches to Fundamental Physics

Jonathan Gorard
2021-04-29

Proofs as programs: challenges and strategies for program synthesis

Shaowei Lin
2021-04-22

Topos theory and measurability

Asgar Jamneshan
2021-04-15

Noncrossing hyperchords and free probability

Joachim Kock
2021-04-08

Reasoning in an infinity-topos with homotopy type theory

Dan Christensen
2021-04-01

Mathematics in the 21st century

John Baez
2021-03-25

The logic of contextuality

Samson Abramsky
2021-03-11

Relative topology, motion planning, and coverage problems

Gunnar E. Carlsson
2021-02-18

Comodels of an algebraic theory

Richard Garner
2021-02-11

Poly: a category of remarkable abundance

David Spivak
2021-02-04

Hybrid systems as coalgebras: Lyapunov morphisms for Zeno stability

Joe Moeller
2026-06-11

The projection formula, extranatural transformations and surface diagrams

Simon Willerton
2026-05-28

Demystifying Codensity Monads via Duality

Stefan Milius
2026-05-21

Many Logics, One Methodology — On the Virtues of LogiKEy in Computational Metaphysics and Ontology

Christoph Benzmueller
2026-05-07

Total Functional Programming, Reloaded

Jeremy Gibbons
2026-04-30

Control, Complete, Compute: Rig Categories in Quantum Computing

Chris Heunen
2026-04-23

Containers and Comodule Representations of Second-Order Functionals

Danel Ahman
2026-04-09

Classically laughable theorems

Andrej Bauer
2026-04-02

BV-Categories and Higher-Order Quantum Theory

James Hefford
2026-03-19

What is a monoid?

Paul Levy
2026-03-12

The Eckmann-Hilton argument in duoidal categories

Marcelo Aguiar
2026-03-05

Properties for the People

Benjamin Pierce
2026-02-26

Autoformalization and the future of math and science

Patrick Shafto
2026-02-19

Combinatory Completeness in Structured Multicategories

Chad Nester
2026-02-12

Designing and developing an industrial-strength programming language

Dan Ghica
2026-02-05

The category of schemes is abelian (and other obviously-false true things)

Inna Zakharevich
2026-01-29

Cospans of finite sets

John Baez
2025-12-11

Concrete syntax matters, actually

Slim Lim
2025-12-04

Commutative rings, bispans, and their equivariant analogues

Rune Haugseng
2025-11-06

Two-dimensional Kripke Semantics

Alex Kavvos
2025-11-06

What's up with AI?

Terry Winograd
2025-10-30

Symmetry beyond group and its description by braided fusion category

Xiao-Gang Wen
2025-10-23

Syntax and semantics for mechanical processes

Cole Comfort
2025-10-16

Behavioural Metrics via Functor Lifting – A Coalgebraic Approach

Barbara König
2025-10-09

Instances of models of double theories

Kevin Carlson
2025-10-02

A double category of transducers

Fosco Loregian
2025-09-25

Double categorical equivalences

Maru Sarazola
2025-09-18

Dependetopes and Higher Generalized Algebraic Theories

Eric Finster
2025-09-11

Towards a mathematical theory of intentional systems

Nathaniel Virgo
2025-09-04

CAP — a categorical (re)organization of computer algebra

Mohamed Barakat
2025-07-17

Abstractions for Real People

Brendan Fong
2025-07-10

ZX Calculus and Fault-tolerant quantum computing

Aleks Kissinger
2025-07-03

Opetopic shapes, combinatorially

Pierre-Louis Curien
2025-06-26

Articulating the Structure of Reasons: Logical Expressivism and Implication-Space Semantics

Robert Brandom
2025-06-19

Cartesian Fermat Categories, a new class of Cartesian Differential Categories

Jean-Simon Lemay
2025-06-12

Organisation of the Information Flow in the Perception-Action Loop

Daniel Polani
2025-05-29

Random Variables, Independence Structures and Dagger Categories of Relations

Dario Stein
2025-05-22

Duality for complete atomic partial Boolean algebras

Samson Abramsky
2025-05-15

Combinatorial foundation for planar string diagrams

Amar Hadzihasanovic
2025-05-08

Distillation systems as models of homotopy colimits

Kristine Bauer
2025-05-01

V-graded categories as a setting for enrichment and actions of monoidal categories V

Rory Lucyshyn-Wright
2025-04-24

Update rules of Pearl and Jeffrey

Bart Jacobs
2025-04-17

Beyond Tech Solutionism: Challenges of unlocking under-served community knowledge

Kate Fleming
2025-04-10

A (virtual) double category theorist's perspective on polynomials

Nathanael Arkor
2025-04-03

Geometric principles of data visualization

Juergen Jöst
2025-03-27

Language, Technology, & Care

B. Scot Rousse
2025-03-20

(Co)algebraic analysis of social systems: from graphs to hypergraphs

Nina Otter
2025-03-13

Representable Behaviour in Double Categorical Systems Theory

Matteo Capucci
2025-03-06

A categorical approach to Lyapunov stability

Joe Moeller
2025-02-27

Tensor Species: The Theory and Practice of Neural Networks

Andrew Dudzik
2025-02-13

The rabbit calculus: convolution products on double categories and categorification of rule algebra

Paul-Andre Mellies
2025-02-06

Kleisli constructions for pseudomonads

Adrian Miranda
2025-01-31

Engineering practice and the potential role of CT in systems engineering

Eswaran Subrahmanian
2024-12-12

Collective grassroots knowledge generation with lab discourse graphs

Matthew Akamatsu
2024-12-05

Unravelling the "Unreasonable Effectiveness" of Mathematics

Arezoo Islami
2024-11-14

Graphical Methods in Quantum Cryptography

Carl Miller
2024-11-07

Partial Markov Categories

Mario Román
2024-10-31

Compact Proofs: Measuring Quality of Understanding with a Compression-Based Metric

Jason Gross
2024-10-24

Quantitative results for stochastic processes

Thomas Powell
2024-10-16

Cubical types for the working formalizer

Amélia Liao
2024-10-03

Online communities as model systems for commons governance

Seth Frey
2024-09-26

What is the Identity operator?

Chris Fields
2024-09-19

Semantics for Reactive Probabilistic Programming

Christine Tasson
2024-09-12

Polynomial Interfaces

Spencer Breiner
2024-09-05

Totally Live Programming and Proving in Hazel

Cyrus Omar
2024-08-29

How to Make Mathematicians Into Programmers (And Vice Versa)

Will Chrichton
2024-08-22

The Automation of Mathematics from an Anthropological Perspective

Rodrigo Ochigame
2024-08-15

A generalization of inversion using Bayes' rule with applications to quantum

Arthur J Parzygnat
2024-08-08

On Taming Differentiable Logics

Kathrin Stark
2024-08-01

From gs-monoidal to cartesian categories: a structural analysis

Fabio Gadducci
2024-07-11

Topological Data Analysis of Spatial Systems

Mason Porter
2024-06-27

Parametric Profunctor Preoptics

Bartosz Milewski
2024-06-13

Three toposes for probability and randomness

Alex Simpson
2024-06-06

The Fundamental Theorem of Calculus: point-free

Steve Vickers
2024-05-30

Why bother to do topology that way? After all, the logic is even more constrained than constructive reasoning, and we still don’t know how far it reaches.

Steven Vickers “Topical categories of domains”, Mathematical Structures in Computer Science 9 (1999)
Bas Spitters, Steven Vickers and Sander Wolters “Gelfand spectra in Grothendieck toposes using geometric mathematics”, Electronic Proceedings in Theoretical Computer Science 158 (2014)
Steven Vickers “The Fundamental Theorem of Calculus point-free, with applications to exponentials and logarithms”, arXiv:2312.05228

Monoidal bicategories, differential linear logic, and analytic functors

Nicola Gambino
2024-05-23

Effectful trace semantics via effectful streams

Elena Di Lavore
2024-05-16

Categories of Classes for Collection Monads

Eugenio Moggi
2024-05-09

Diagrammatic Algebra of First Order Logic

Filippo Bonchi
2024-05-02

Co-Design of Complex Systems: From Autonomy to Future Mobility

Gioele Zardini
2024-04-25

Certainty or Intelligence: Pick One!

Edward Lee
2024-04-18

Uniting Game Theory, Math Stars, and Actors To Build Human Intelligence in the AI Age

Po-Shen Loh
2024-04-04

Sociotechnical infrastructure for mathematics research

Steven Clontz
2024-03-28

Polynomial functors — from elementary arithmetic to infinity-operads

Joachim Kock
2024-02-22

Free bicompletion of categories revisited (part 1)

André Joyal
2024-02-15

Cauchy Completeness and Adjoints in Double Categories

Susan Niefield
2024-02-08

Cohomological aspects of information

Juan Pablo Vigneaux
2024-01-25

Aspects of a Mathematical Theory of Data

John Cartmell
2024-01-18

The functorial difference operator

Robert Paré
2024-01-11

Higher topos theory and Goodwillie Calculus

André Joyal
2023-12-14

Models for (∞,n)-categories with discreteness conditions

Julie Bergner
2023-12-07

Who Owns Mathematics: A Question of Identity

Minhyong Kim
2023-11-30

Normalising ethical reasoning for mathematicians

Maurice Chiodo
2023-11-16

(Higher) category theory in Cat^#

Brandon Shapiro
2023-11-02

Entropy and diversity: the axiomatic approach

Tom Leinster
2023-10-26

Simplicial delta versus fat delta in higher category theory

Simona Paoli
2023-10-19

Programming for the Planet

Dominic Orchard
2023-10-12

Synthetic Domains in the 21st Century

Jonathan Sterling
2023-09-28

Emergent Selves and Unconventional Intelligences: where philosophy and engineering meet

Michael Levin
2023-09-21

Lean 4: Empowering the Formal Mathematics Revolution and Beyond

Leonardo de Moura
2023-09-07

Abstraction Engineering with the Prototype Verification System (PVS)

Nat Shankar
2023-08-31

Quantum Programming via Linear Homotopy Types

Urs Schreiber
2023-08-24

(This is joint work with D. J. Myers, M. Riley and H. Sati.)

Towards Compositional System Dynamics for Public Health

Nathaniel Osgood
2023-06-29

Applying Categorical Thinking to Practical Domains

Jared Culbertson
2023-06-22

Categorical Causality & Systems Theory

Taco Cohen
2023-06-15

Abstraction in programming language theory: Howe's method

Tom Hirschowitz
2023-06-08

How to interpret cotorsion

Alex Martsinkovsky
2023-06-01

As If Category Theory were a Foundation

Elaine Landry
2023-05-25

Proof Certificates in Satisfiability Modulo Theories

Clark Barrett
2023-05-18

Toward a useful category for persistent homology

Chad Giusti
2023-05-11

How Categories Come to Matter: On the history and sociology of categories in modern mathematics

Michael Barany
2023-05-04

Foothills and cathedrals: organising the libraries behind big proofs

Georges Gonthier
2023-04-27

Generalized existential completions and applications

Davide Trotta
2023-04-20

Effective Quantum Certification via Linear Homotopy Types

Urs Schreiber
2023-04-13

To solve this problem we present Linear homotopy type theory (LHoTT) as a programming and certification language for quantum computers with classical control and topologically protected quantum gates, focusing on (1.) its categorical semantics, which is a homotopy-theoretic extension of that of Proto-Quipper and a parameterized extension of Abramsky et al.’s quantum protocols, (2.) its expression of quantum measurement as a computational effect induced from dependent linear type formation and reminiscent of Lee at al.’s dynamic lifting monad but recovering the interacting systems of Coecke et al.’s “classical structures” monads.

(This is joint work with D. J. Myers, M. Riley and H. Sati. Slides will be available at: ncatlab.org/schreiber/show/Quantum+Certification+via+Linear+Homotopy+Types)

Metric spaces, entropic spaces and convexity

Simon Willerton
2023-03-30

Dual algebraic structures and enrichment

Christina Vasilakopoulou
2023-03-23

Category theory outreach panel

Riehl, Bradley, Cheng, Dancstep, and Lugg
2023-03-16

Philosophical perspectives on category theory

David Corfield
2023-03-09

Algebraic and Geometric Models for Space Networking

Justin Curry
2023-03-02

Towards a Higher-Order Mathematical Operational Semantics

Sergey Goncharov
2023-02-16

Nuclear ideals in monoidal *-categories

Prakash Panangaden
2023-02-09

Fuzzy type theory

Paige North
2023-02-02

Univalent Foundations and Applied Mathematics

Andrei Rodin
2022-12-15

Implicative algebras: a new foundation for realizability and forcing

Alexandre Miquel
2022-12-08

Electrical circuits with string diagrams

Pawel Sobocinski
2022-12-01

From the Universality of Mathematical Truth to the Interoperability of Proof Systems

Gilles Dowek
2022-11-10

A double-categorical approach to lenses via algebraic weak factorisation systems

Bryce Clarke
2022-11-03

Mathematical Information Retrieval: Searching with Formulas and Text

Richard Zanibbi
2022-10-27

Turing categories

Robin Cockett
2022-10-20

Working Compositions for Correct Execution of Robot Task Specifications

Dan Koditschek
2022-10-13

M. H. Raibert, Legged Robots That Balance. Cambridge: MIT Press, 1986.
D. E. Koditschek, “What Is Robotics? Why Do We Need It and How Can We Get It?,” Annu. Rev. Control Robot. Auton. Syst., vol. 4, no. 1, pp. 1–33, May 2021, doi: 10.1146/annurev-control-080320-011601.
R. J. Full and D. E. Koditschek, “Templates and anchors: neuromechanical hypotheses of legged locomotion on land,” J. Exp. Biol., vol. 202, pp. 3325–3332, 1999.
A. De, S. A. Burden, and D. E. Koditschek, “A hybrid dynamical extension of averaging and its application to the analysis of legged gait stability:,” Int. J. Robot. Res., vol. 37, no. 2–3, pp. 266–286, Mar. 2018, doi: 10.1177/0278364918756498.
R. R. Burridge, A. A. Rizzi, and D. E. Koditschek, “Toward a systems theory for the composition of dexterous robot behaviours,” Robot. Res. Seventh Int. Symp. ISRR’95, pp. 149–161.
V. Vasilopoulos et al., “Reactive Semantic Planning in Unexplored Semantic Environments Using Deep Perceptual Feedback,” IEEE Robot. Autom. Lett., vol. 5, no. 3, pp. 4455–4462, Jul. 2020, doi: 10.1109/LRA.2020.3001496.
V. Vasilopoulos, Y. Kantaros, G. Pappas, and D. Koditschek, “Reactive Planning for Mobile Manipulation Tasks in Unexplored Semantic Environments,” IEEE Int. Conf. Robot. Autom. ICRA, May 2021, [Online]. Available: https://repository.upenn.edu/ese_papers/880
T. T. Topping, V. Vasilopoulos, A. De, and D. Koditschek E., “Composition of Templates for Transitional Pedipulation Behaviors,” in Proc. Int. Symp. Rob. Res., 2019. [Online]. Available: https://repository.upenn.edu/ese_papers/860/
V. Vasilopoulos, G. Pavlakos, K. Schmeckpeper, K. Daniilidis, and D. E. Koditschek, “Reactive Navigation in Partially Familiar Non-Convex Environments Using Semantic Perceptual Feedback,” Int. J. Robot. Res., vol. 41, no. 1, pp. 85–126, Jan. 2022, doi: 10.1177/02783649211048931.
J. Culbertson, P. Gustafson, D. E. Koditschek, and P. F. Stiller, “Formal composition of hybrid systems,” Theory Appl. Categ., vol. 35, no. 45, pp. 1634–1682, Oct. 2020.
A. M. Johnson, S. A. Burden, and D. E. Koditschek, “A hybrid systems model for simple manipulation and self-manipulation systems,” Int. J. Robot. Res., vol. 35, no. 11, pp. 1354–1392, Sep. 2016, doi: 10.1177/0278364916639380.
R. R. Burridge, A. A. Rizzi, and D. E. Koditschek, “Sequential Composition of Dynamically Dexterous Robot Behaviors,” Int. J. Robot. Res., vol. 18, no. 6, pp. 534–555, 1999, doi: 10.1177/02783649922066385.
C. R. Robinson, Dynamical Systems: Stability, Symbolic Dynamics, and Chaos, Second. Boca Raton, FL: CRC Press, 1999. Accessed: Jan. 29, 2017. [Online]. Available: http://imb-biblio.u-bourgogne.fr/Record.htm?record=325212414349&idlist=1
M. D. Kvalheim, P. Gustafson, and D. E. Koditschek, “Conley’s Fundamental Theorem for a Class of Hybrid Systems,” SIAM J. Appl. Dyn. Syst., pp. 784–825, Jan. 2021, doi: 10.1137/20M1336576.

The new era of formalised mathematics and the ALEXANDRIA Project

Angeliki Koutsoukou Argyraki
2022-10-06

Breaking the one-mind-barrier in mathematics using formal verification

Johan Commelin
2022-09-29

What I learned from formalizing Category Theory in Agda

Jacques Carette
2022-09-22

On localizations via homotopies

Eduardo Dubuc
2022-09-15

A synthetic approach to orbifolds

David Jaz Myers
2022-09-08

Applied Measure Theory for Composable Statistical Modeling

Chad Scherrer
2022-09-01

Categorification of Negative Information

Andrea Censi
2022-08-25

Combining learning and deduction over formal math corpora

Josef Urban
2022-07-07

Parsing as a lifting problem and the Chomsky-Schützenberger representation theorem

Noam Zeilberger
2022-06-30

Joint work with Paul-André Melliès.

P.-A. Melliès and N. Zeilberger, Functors are type refinement systems, POPL 2015
P.-A. Melliès and N. Zeilberger, Parsing as a lifting problem and the Chomsky-Schützenberger representation theorem, 2022 (to appear)

Ethics Washing in AI

Moshe Vardi
2022-06-23

Logico-pluralistic exploration of foundational theories with computers

Christoph Benzmueller
2022-06-16

Fundamentals of Compositional Rewriting Theory

Nicolas Behr
2022-06-09

This presentation is based upon [1] (joint work with R. Harmer and J. Krivine).

Finally, I will provide an overview of open questions and potential fruitful cross-connections of crDC theory with the TIC and broader ACT communities.

N. Behr, R. Harmer and J. Krivine, “Fundamentals of Compositional Rewriting Theory”, https://arxiv.org/abs/2204.07175
N. Behr, J. Krivine, J.L. Andersen, D. Merkle (2021), “Rewriting theory for the life sciences: A unifying theory of CTMC semantics”, https://doi.org/10.1016/j.tcs.2021.07.026
N. Behr, B.S. Bello, S. Ehmes, R. Heckel (2021), “Stochastic Graph Transformation For Social Network Modeling”, https://doi.org/10.4204/EPTCS.350.3
N. Behr (2021), “On Stochastic Rewriting and Combinatorics via Rule-Algebraic Methods”, http://dx.doi.org/10.4204/EPTCS.334.2

Sheaf Cohomology in Univalent Type Theory

Thierry Coquand
2022-06-02

Entropy as an Operad Derivation

Tai-Danae Bradley
2022-05-26

Learning Weighted Automata over Principal Ideal Domains

Alexandra Silva
2022-05-19

The countable reals

Andrej Bauer
2022-05-12

Joint work with James E. Hanson from the University of Maryland.

Rethinking language

John Terilla
2022-05-05

Compact totally separated types in constructive univalent type theory

Martín Escardó
2022-04-28

Making Microworlds: A Framework for Making Sense by Making Things

Leo McElroy
2022-04-14

When an elementary quotient completion is a quasitopos

Giuseppe Rosolini
2022-04-07

Lessons from failing distributive laws

Maaike Zwart
2022-03-31

Zen and the art of ∞-categories

Dominic Verity
2022-03-24

There must be a better way!

E. Riehl, M. Shulman, A type theory for synthetic ∞-categories, High. Struct. 1 (2017) 147224.
E. Riehl, D. Verity, Elements of ∞-category theory, Cambridge University Press, 2022.
J. Weinberger, A synthetic perspective on (∞,1)-category theory: Fibrational and semantic aspects, arXiv Preprint arXiv:2202.13132. (2022).

The logic of social influence in networks

Zoé Christoff
2022-03-17

Making concurrency functional

Glynn Winskel
2022-03-03

Compositional Intelligence

Bob Coecke
2022-02-24

Ethics in AI, not Ethics of AI

David Danks
2022-02-17

Phase Distinctions in Type Theory

Robert Harper
2021-12-09

Categories of diagrams in data migration and computational physics

Evan Patterson
2021-12-02

The rise of quantitative category theory

Paolo Perrone
2021-11-18

Formal mathematics, dependent type theory, and the Topos Institute

Jeremy Avigad
2021-11-04

Doubly Lax Colimit of Double Categories with Applications

Dorette Pronk
2021-10-28

Cubical setting for Discrete Homotopy Theory

Chris Kapulkin
2021-10-21

A topos view of axioms of choice for finite sets

Andreas Blass
2021-10-14

Cubical Methods in Homotopy Type Theory and Univalent Foundations

Anders Mortberg
2021-10-07

Algebraic theories with string diagrams

Pawel Sobocinski
2021-09-30

Abstract homotopy theory for topological data analysis

Andrew J. Blumberg
2021-09-23

Understanding free infinity-categories

Jamie Vicary
2021-09-16

Tensor products, multimaps and internal homs

John Bourke
2021-09-09

MMT: A UniFormal Approach to Knowledge Representation

Florian Rabe
2021-09-02

Cats and Types: Best Friends?

Conor McBride
2021-08-26

Categorical Explicit Substitutions

Valeria de Paiva
2021-08-19

What is the point of Lean's maths library?

Kevin Buzzard
2021-08-12

From 2-rigs to lambda-rings

Todd Trimble
2021-08-05

Topological Inspiration for Infinity Modular Operads

Marcy Robertson
2021-07-29

What is monoidal topology?

Walter P Tholen
2021-07-22

Categorical differential structures and their role in abstract machine learning

Geoffrey Cruttwell
2021-07-08

Formalising Contemporary Mathematics in Simple Type Theory

Lawrence Paulson
2021-07-01

From comonads to calculus

Kathryn Hess
2021-06-24

Sheaf representation of monoidal categories

Chris Heunen
2021-06-17

A category of hybrid systems

Eugene Lerman
2021-06-10

Model Structures from Models of HoTT

Steve Awodey
2021-06-03

Two-dimensional semantics of homotopy type theory

Michael Shulman
2021-05-27

The law of large numbers in categorical probability

Tobias Fritz
2021-05-20

Quotient completions for topos-like structures

Maria Emilia Maietti
2021-05-13

[HJP80] J.M. Hyland, P. T. Johnstone and A.M.Pitts. Tripos theory. Math. Proc. Cambridge Philos. Soc. 88, 205-232, 1980
[M09] M.E. Maietti. A minimalist two-level foundation for constructive mathematics. Annals of Pure and Applied Logic, 160(3): 319-354, 2009
[MR13] M.E. Maietti and G. Rosolini. Elementary quotient completion. Theory and Applications of Categories, 27(17): 445–463, 2013
[MR15 ] M.E. Maietti and G. Rosolini. Unifying Exact Completions. Applied Categorical Structures 23(1): 43-52, 2015
[MPR17] M.E. Maietti, F. Pasquali and G. Rosolini. Triposes, exact completions, and Hilbert’s ε-operator. Tbilisi Mathematical Journal. 10(3): 141-66, 2017
[Me03] M. Menni. A characterization of the left exact categories whose exact completions are toposes. Journal of Pure and Applied Algebra, 3(177): 287-301, 2003
[MM21] M.E. Maietti, S. Maschio. A predicative variant of Hyland’s Effective Topos. To appear in The Journal of Symbolic Logic

Contractibility as uniqueness

Emily Riehl
2021-05-06

Fast Diagrammatic Reasoning and Compositional Approaches to Fundamental Physics

Jonathan Gorard
2021-04-29

Proofs as programs: challenges and strategies for program synthesis

Shaowei Lin
2021-04-22

Topos theory and measurability

Asgar Jamneshan
2021-04-15

Noncrossing hyperchords and free probability

Joachim Kock
2021-04-08

Reasoning in an infinity-topos with homotopy type theory

Dan Christensen
2021-04-01

Mathematics in the 21st century

John Baez
2021-03-25

The logic of contextuality

Samson Abramsky
2021-03-11

Relative topology, motion planning, and coverage problems

Gunnar E. Carlsson
2021-02-18

Comodels of an algebraic theory

Richard Garner
2021-02-11

Poly: a category of remarkable abundance

David Spivak
2021-02-04