7th International Conference on Applied Category Theory
40th Conference on Mathematical Foundations of Programming Semantics
ACT & MFPS • Oxford • June 2024
ACT & MFPS List of Talks
Joint ACT & MFPS keynote

Andrew Pitts (University of Cambridge) — Toposes of Finitely Supported MSets
For at least the last 25 years several toposes of finitely supported
Msets (for various monoids M) have played an important role in my
work on logic and computer science, but in apparently unconnected
ways. I feel that this kind of topos is trying to get my attention. So
I will use this talk to tell you what they are; some of their nice
(and not so nice) properties; and a little about the contexts in which
they have arisen for me, namely the mathematics of syntax involving
binders and the semantics of univalent type theories. My hope is that
you will also find them useful, or be able to tell me something about
them that I don't know. For example, I do not know an abstract
characterisation of this class of topos. [slides]
Joint ACT & MFPS special session in memory of Phil Scott
Organiser: Rick Blute (University of Ottawa). Chair: Andrew Pitts.

Rick Blute (University of Ottawa) — Proofs, Types and Hexagons
Phil’s book with Jim Lambek “Introduction to HigherOrder Categorical Logic” is a seminal work in category theory. It cemented in the minds of many of us working in the field the idea that the best approach to studying logical systems was to form a category whose objects are formulas and arrows are proofs of entailments. Extensions of this idea are an obsession of the categorical logic community to this day.
One of the most interesting extensions involves representing formulas as multivariant functors and thus proofs become dinatural transformations, the hexagons of the title. The problem/challenge that arises is that these transformations need not compose. This has led to a great deal of interesting category theory, much of which Phil contributed to. I’ll review some of these results, especially those relating to linear logic. [slides]

Samson Abramsky (University of Oxford) — Retracing GoI with Phil
I will describe my collaboration with Phil Scott and Esfandiar Haghverdi on categorical semantics of Geometry of Interaction. I will say something about the context of this work, and where it led. [slides]

Robin Cockett (University of Calgary) — Phil Scott and Occam's Razor
.In Phil's book with Lambek the authors confess they have "axes to grind". One of these
is "We decry over zealous application of Occam's razor."
Despite this, the book deploys Occam's razor to good effect in order to describe how models of the untyped lambda calculus can be derived. The talk traces these ideas forward leading into how they influenced the speaker's work.

Mark Lawson (HeriotWatt University) —
Coordinatizing an MValgebra by a Boolean inverse monoid
Both MValgebras (which arise from multiple valued logic)
and Boolean inverse monoids (which partake in a generalization of classical Stone duality)
are generalizations of Boolean algebras.
The question is: how are they related?
Phil Scott and I proved that every countable MValgebra can be coordinatized
by a suitable Boolean inverse monoid (in a sense analogous to classical work by von Neumann).
I shall assume no prior exposure to MValgebras or Boolean inverse monoids
in my talk.
(Phil’s obituary in the CMS Notes.)
MFPS invited speakers

Bob Atkey (University of Strathclyde) — Polynomial Time and Dependent Types
Dependent Type Theory is inherently computational. Constructions and
proofs in Type Theory are programs that can be executed to produce
results. However, all these programs and explanations are built with
no regard for computational complexity within the theory, meaning that
constructions cannot reason or rely on complexity bounds, and
arguments that rely on complexity restrictions lie outwith the grasp
of Type Theory. To address this, I will talk about combining
techniques from Implicit Computational Complexity with Dependent Type
Theory to attempt to bring resource consciousness to Type Theory.

Philippa Gardner (Imperial College, London, UK) — Computational Symbolic Execution for Overapproximating and Underapproximating Reasoning
A relatively recent challenge has been to develop symbolicexecution techniques and tools that are functionally compositional with simple function specifications that can be used in broader calling contexts. The technical breakthrough came with the introduction of separation logics for reasoning about partial mutable state, leading to compositional symbolic execution tools being developed in academia and industry. Many of these tools have been grounded on a formal foundation, but either the function specifications are validated with respect to the underlying symbolic semantics of the engine, with no meaning outside the tool, or there is a large gulf between the theory and the implementations of the tools. In this talk, I will introduce a formal compositional symbolic execution engine which creates and uses function specifications from an underlying separation logic and provides a sound theoretical foundation for, and indeed was partially inspired by, the Gillian platform. This is achieved by providing an axiomatic interface which describes the properties of the consume and produce functions for updating the symbolic state when calling function specifications, a technique used by VeriFast, Viper and Gillian but not previously characterised independently of the tool. A surprising property is that our semantics provides a common foundation for both correctness and incorrectness reasoning, with the difference in the underlying engine only amounting to the choice to use satisfiability or validity. We use this insight to extend the Gillian platform with incorrectness reasoning, developing automatic true bugfinding using incorrectness biabduction, which our engine incorporates by creating fixes from missingresource errors. We have shown that the Gillian implementation of the consumer and producer functions satisfy the properties described by our axiomatic interface, and evaluate our new Gillian platform by using the Gillian instantiation to C. This instantiation is the first tool to support both correctness and incorrectness reasoning, as well as being grounded on a common formal compositional symbolic execution engine. (Authors: Andreas Lööw, Daniele Nantes Sobrinho, SachaElie Ayoun, Caroline Cronjäger, Petar Maksimović and Philippa Gardner.)

Ohad Kammar (University of Edinburgh) — Semantic foundations for typedriven probabilistic modelling
The last few years have seen several breakthroughs in the semantic
foundations of probabilistic and statistical modelling. Types show
clear promise in organising intricate models and the inference
algorithms we use to fit them to data. I will present a typerich and
straightforward model, the quasi Borel space, and survey recent and
ongoing developments in this area. [slides]

Catuscia Palamidessi (INRIA Saclay & LIX, France) — Information Structures for Privacy and Fairness
The increasingly pervasive use of big data and machine learning is raising various ethical issues, in particular privacy and fairness.
In this talk, I will discuss some frameworks to understand and mitigate the issues, focusing on iterative methods coming from information theory and statistics.
In the area of privacy protection, differential privacy (DP) and its variants are the most successful approaches to date. One of the fundamental issues of DP is how to reconcile the loss of information that it implies with the need to preserve the utility of the data. In this regard, a useful tool to recover utility is the Iterative Bayesian Update (IBU), an instance of the famous ExpectationMaximization method from Statistics. I will show that the IBU, combined with the metric version of DP, outperforms the stateofthe art, which is based on algebraic methods combined with the Randomized Response mechanism, widely adopted by the Big Tech industry (Google, Apple, Amazon, ...). Furthermore I will discuss a surprising duality between the IBU and one of the methods used to enhance metric DP, that is the BlahutArimoto algorithm from RateDistortion Theory. Finally, I will discuss the issue of biased decisions in machine learning, and will show that the IBU can be applied also in this domain to ensure a fairer treatment of disadvantaged groups.
MFPS special session on the semantics of nonwellfounded and circular proofs
Organisers: Anupam Das and Abhishek De (University of Birmingham). Chair: Abishek De.

Farzad Jafarrahmani (LMCRC, Huawei) — Focused orthogonality as denotations of circular and nonwellfounded proofs
This talk investigates the question of denotational invariants of nonwellfounded and circular proofs of the linear logic with least and greatest fixpoints. While nonwellfounded and circular proof theory has made significant progress in the last twenty years, the corresponding denotational semantics is still underdeveloped. First, we explore a theory of fixpoint constructions in focused orthogonality categories and present a lifting theorem for initial algebras and final coalgebras. These constructions crucially hinge on the insight that focused orthogonality categories are relational fibrations. We then demonstrate that assuming a CPO structure on our category allows the focused orthogonality construction to provide a model for nonwellfounded proofs. Several properties of the semantics will be discussed, including its soundness, the relationship between totality (orthogonality) and validity, and the semantic content involved in translating finitary proofs to circular proofs. Finally, the talk focuses on circular proofs, aiming to leverage their regularity to define the interpretation function inductively. We argue why the usual validity condition is too general for this purpose, while a fragment of circular proofs—strongly valid proofs—constitutes a wellbehaved class for such an inductive interpretation.

Farzaneh Derakhshan (Illinois Tech) — SessionTyped Recursive Processes and Infinitary Proofs
Session types describe the communication behavior of interacting processes. Binary session types, in which each channel has two endpoints, corresponds to intuitionistic linear logic by a CurryHoward interpretation of propositions as types, proofs as programs, and cut reduction as communication. This interpretation provides a solid foundation for reasoning about the behavior of sessiontyped processes. For example, termination of a process can be inferred from the cut elimination property of its underlying proof. However, as soon as we add recursive session types, we abandon this correspondence and lose our solid ground. From the programming perspective, it means that we can no longer exploit the cut elimination property to guarantee termination. In this talk, I show how we can revitalize the logical foundation for recursive binary sessiontyped processes by using infinitary proof systems for linear logic. We show that if we refine recursive types as least and greatest fixed points and impose a guard condition on recursive processes, we can still guarantee meaningful communication, ensuring that a program always terminates either in an empty configuration or one attempting to communicate along external channels.

Gianluca Curzi (University of Gothenburg) — Computational aspects of cyclic and nonwellfounded proofs
Nonwellfounded proof theory studies a more permissive notion of proof seen as a possibly infinite (but finitely branching) tree structure. Cyclic proofs are special nonwellfounded proofs whose underlying tree is regular, thereby they admit a finite presentation in terms of finite (possibly cyclic) graphs. Over the years, cyclic and nonwellfounded proofs have received growing interest, especially given their capability of subsuming various forms of (co)inductive reasoning and, under a computational reading, (co)recursion mechanisms. This talk is meant to provide a bird's eye view of the stateoftheart research around the computational analysis of cyclic and nonwellfounded proof systems, with special attention to the speaker's contribution on the topic. More specifically, the talk will examine a number of systems, spanning from those expressing complex forms of ordinal and higherorder recursion down to those implementing quickly converging recursion schemes suitable for complexitytheoretic considerations.
Contributed talks
Jump to ACT contributed talks or MFPS contributed talks.
ACT contributed talks
 Convergence of martingales via enriched dagger categories — Paolo Perrone, Ruben Van Belle [pdf]
 The AldousHoover Theorem in Categorical Probability — Leihao Chen, Tobias Fritz, Tomáš Gonda, Andreas Klingler, Antonio Lorenzin [pdf] [slides]
 A Category Theoretic Approach to Approximate Game Theory — Neil Ghani [pdf]
 Copycomposition for probabilistic graphical models — Toby St Clere Smithe [pdf] [slides]
 Combs, Causality and Contractions in Atomic Markov Categories — Dario Maximilian Stein, Márk Széles [pdf]
 Representing Knowledge and Querying Data using DoubleFunctorial Semantics — Michael Lambert, Evan Patterson [pdf] [slides]
 Partial and Relational Algebraic Theories — Chad Nester [pdf] [slides]
 Fibrational perspectives on determinization of finite state automata — Thea Li [pdf] [slides]
 Presenting Profunctors — Gabriel Goren Roig, Joshua Meyers, Emilio Minichiello [pdf] [slides]
 Proqueries and Praqueries — Gabriel Goren Roig, Joshua Meyers, Emilio Minichiello, Ryan Wisnesky [pdf] [slides]
 Pattern runs on matter: The free monad monad as a module over the cofree comonad comonad — Sophie Libkind, David Spivak [pdf] [slides]
 Organizing physics with open energydriven systems — Owen Lynch, David Spivak, Matteo Capucci [pdf] [slides]
 Compositional statistical mechanics, entropy and variational free energy — Grégoire SergeantPerthuis [pdf]
 ModelCollab: Software for Compositional Modeling — John Carlos Baez, Xiaoyan Li, Nathaniel D. Osgood [pdf]
 ViCAR: Visualizing Categories with Automated Rewriting in Coq — Bhakti Shah, William Spencer, Laura Zielinski, Ben Caldwell, Adrian Lehmann, Robert Rand [pdf] [slides]
 Towards a Unified Theory of TimeVarying Data — Benjamin Merlin Bumpus, James Fairbanks, Martti Karvonen, Wilmer Leal, Frédéric Simard [pdf]
 Overview of progress — Adjoint School [pdf]
 Inference on posetshaped diagrams in the category of Markov kernels — Grégoire SergeantPerthuis, Nils Ruet [pdf] [slides]
 Categorical Decision Theory — Marcus Pivato [pdf] [slides]
 How Nice is this Functor? Two Squares and Some Homology go a Long Way — Benjamin Merlin Bumpus, Daniel Rosiak, Caterina Puca, Fabrizio Romano Genovese, James Fairbanks [pdf] [slides]
 Expansion of the (category) theory of metric spaces and fuzzy simplicial sets and their applications to data analysis — Lukas Barth, Jürgen Jost, Thomas Jan Mikhail, Janis Keck, Parvaneh Joharinad, Fatemeh Hannaneh Fahimi Sheyjani [pdf] [slides]
 Homotopical characterization of strong contextuality — Aziz Kharoof, Cihan Okay [pdf] [slides]
 Categorified Path Calculus — Simon Burton [pdf] [slides]
 Effectful streams — Filippo Bonchi, Elena Di Lavore, Mario Román [pdf]
 Monoidal Streams and Probabilistic Dataflow with DisCoPy — Alexis Toumi, Richie Yeung, Boldizsár Poór, Giovanni de Felice [pdf]
 Equivariant stochastic neural networks in Markov categories — Rob Cornish [pdf] [slides]
 Generalized Gradient Descent is a Hypergraph Functor — Tyler E Hanks, Matthew Klawonn, James Fairbanks [pdf]
 CatGrad: A Categorical Compiler for Deep Learning — Paul W Wilson [pdf]
 A Convenient Topological Setting for HigherOrder Probability Theory — Benedikt Peterseim [pdf] [slides]
 Nogo theorems: Polynomial comonads that do not distribute over distribution monads — Nihil Shah, Amin Karamlou [pdf] [slides]
 High schoolers excel at Oxford postgraduate quantum exam: experimental evidence in support of quantum picturalism — Bob Coecke, Aleks Kissinger, Stefano Gogioso, Selma Dundar Coecke, Caterina Puca, Lia Yeh, Muhammad Hamza Waseem, Vincent WangMascianica, Sieglinde Pfaendler, Thomas Cervoni, Ferdi Tomassini, Vincent Anandraj, Peter Sigrist [pdf]
 Graphical Symplectic Algebra — Robert I Booth, Titouan Carette, Cole Comfort [pdf] [slides]
 Complete equational theories for classical and quantum Gaussian relations — Robert I Booth, Titouan Carette, Cole Comfort [pdf] [slides]
 A Profunctorial Semantics for Quantum Supermaps — James Hefford, Matt Wilson [pdf] [slides]
 A Coalgebraic Model of Quantum Bisimulation — Lorenzo Ceragioli, Elena Di Lavore, Giuseppe Lomurno, Gabriele Tedeschi [pdf] [slides]
 Completeness of graphical languages for finite dimensional Hilbert spaces — Razin A. Shaikh, Boldizsár Poór, Quanlong Wang [pdf] [slides]
 An operadic approach to convexity — Redi Haderi [pdf]
 Universal recursive preference structures — Marcus Pivato [pdf] [slides]
 Partial Combinatory Algebras for Intensional Type Theory — Sam Speight [pdf] [slides]
 The Grothendieck construction for delta lenses — Bryce Clarke [pdf] [slides]
 Abstract Kleisli structures on 2categories — Adrian Miranda [pdf] [slides]
 Learners are Almost Free Compact Closed — Mitchell Riley [pdf] [slides]
 Monoidal Optics are Universal — Matt Earnshaw, James Hefford, Mario Román [pdf] [slides]
 Reinforcement Learning in Categorical Cybernetics — Jules Hedges, Riu Rodriguez Sakamoto [pdf] [slides]
 A Compositional Framework for FirstOrder Optimization — Tyler E Hanks, Matthew Klawonn, Matthew Hale, Evan Patterson, James Fairbanks [pdf]
 Reverse Faà di Bruno’s Formula — JS Pacaud Lemay, Aaron Biggin [pdf] [slides]
 A Fully Compositional Theory of Sequential Digital Circuits — George Kaye, Dan Ghica, David Sprunger [pdf] [slides]
 HigherOrder DisCoCat (PeirceLambekMontague semantics) — Alexis Toumi, Giovanni de Felice [pdf] [slides]
 Disconnection Rules are Complete for Chemical Reactions — Leo Lobski, Fabio Zanasi, Ella Melissa Gale [pdf] [slides]
 Towards Compositional Interpretability for XAI — Sean Tull, Robin Lorenz, Stephen Clark, Bob Coecke [pdf] [slides]
MFPS contributed talks
 Inferentialist Resource Semantics — Alexander Gheorghiu, Tao Gu and David Pym [pdf] [slides]
 Amortized Analysis via Coalgebra — Harrison Grodin and Robert Harper [pdf] [slides]
 On Kleisli extensions and decorated trace semantics — Daniel Luckhardt, Harsh Beohar and Sebastian Küpper [pdf] [slides]
 Typed Nondeterminism in Concurrent Calculi: The Eager Way — Bas van den Heuvel, Daniele NantesSobrinho, Joseph Paulus and Jorge A — Pérez [pdf] [slides]
 Linear Arboreal Categories — Samson Abramsky, Yoàv Montacute and Nihil Shah [pdf]
 An Ultrametric for Cartesian Differential Categories for Taylor Series Convergence — JeanSimon Lemay [pdf] [slides]
 On a fibrational construction for optics, lenses, and Dialectica categories — Matteo Capucci, Bruno Gavranovic, Abdullah Malik, Francisco Rios and Jonathan Weinberger [pdf]
 Implicit automata in λcalculi III: affine planar stringtostring functions — Cécilia Pradic and Ian Price [pdf] [slides]
 The Functional Machine Calculus III: Choice (Early Announcement) — Willem Heijltjes [pdf] [slides]
 Parametricity via Cohesion — C.B  Aberlé [pdf] [slides]
 Relational parametricity in the presence of GADTs (Early Announcement) — Pierre Cagne and Patricia Johann [pdf]
 Compositional models for imprecise probability (Early Announcement) — Jack LiellCock and Sam Staton [pdf] [slides]
 A strong nominal semantics for fixedpoint constraints — Ali Khan Caires Ribeiro, Maribel Fernandez and Daniele NantesSobrinho [pdf] [slides]
 Continuous Domains for Function Spaces Using Spectral Compactification — Amin Farjudian and Achim Jung [pdf] [slides]
 Costsensitive computational adequacy of higherorder recursion in synthetic domain theory — Yue Niu, Jonathan Sterling and Robert Harper [pdf] [slides]
 Algebraic Reasoning over Relational Structures — Jan Jurka, Stefan Milius and Henning Urbat [pdf] [slides]
 GATlab: Modeling and Programming with Generalized Algebraic Theories — Owen Lynch, Kris Brown, James Fairbanks and Evan Patterson [pdf]
 Polynomials in homotopy type theory as a Kleisli category — Elies Harington and Samuel Mimram [pdf] [slides]
 CaTT contexts are finite computads — Thibaut Benjamin, Ioannis Markakis and Chiara Sarti [pdf] [slides]
 Twodimensional Kripke Semantics II: Stability and Completeness — Alex Kavvos [pdf] [slides]
 A Semantic Proof of Generalised Cut Elimination for Deep Inference — Robert Atkey and Wen Kokke [pdf] [slides]
 Positive Focusing is Directly Useful — Beniamino Accattoli and JuiHsuan Wu [pdf] [slides]
Additional sessions
 ACT Industry Session
 ACT session for reporting from the Adjoint School
There will also be a meeting of the Southern Logic Seminar in Oxford during this week. (Separate signup required for this.)