ACT & MFPS List of Talks

Joint ACT & MFPS keynote

Andrew Pitts (University of Cambridge) — Toposes of Finitely Supported M-Sets
For at least the last 25 years several toposes of finitely supported M-sets (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 Higher-Order 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 (Heriot-Watt University) — Co-ordinatizing an MV-algebra by a Boolean inverse monoid
Both MV-algebras (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 MV-algebra can be co-ordinatized by a suitable Boolean inverse monoid (in a sense analogous to classical work by von Neumann). I shall assume no prior exposure to MV-algebras 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 Over-approximating and Under-approximating Reasoning
A relatively recent challenge has been to develop symbolic-execution techniques and tools that are functionally compositional with simple function specifications that can be used in broader calling contexts. The technical break-through 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 bug-finding using incorrectness bi-abduction, which our engine incorporates by creating fixes from missing-resource 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, Sacha-Elie Ayoun, Caroline Cronjäger, Petar Maksimović and Philippa Gardner.)
Ohad Kammar (University of Edinburgh) — Semantic foundations for type-driven 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 type-rich 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 Expectation-Maximization method from Statistics. I will show that the IBU, combined with the metric version of DP, outperforms the state-of-the 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 Blahut-Arimoto algorithm from Rate-Distortion 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 non-wellfounded 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 non-wellfounded proofs
This talk investigates the question of denotational invariants of non-wellfounded and circular proofs of the linear logic with least and greatest fixpoints. While non-wellfounded 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 non-wellfounded 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 well-behaved class for such an inductive interpretation.
Farzaneh Derakhshan (Illinois Tech) — Session-Typed 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 Curry-Howard 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 session-typed 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 session-typed 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 non-wellfounded proofs
Non-wellfounded proof theory studies a more permissive notion of proof seen as a possibly infinite (but finitely branching) tree structure. Cyclic proofs are special non-wellfounded proofs whose underlying tree is regular, thereby they admit a finite presentation in terms of finite (possibly cyclic) graphs. Over the years, cyclic and non-wellfounded 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 state-of-the-art research around the computational analysis of cyclic and non-wellfounded 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 higher-order recursion down to those implementing quickly converging recursion schemes suitable for complexity-theoretic 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 Aldous-Hoover Theorem in Categorical Probability — Leihao Chen, Tobias Fritz, Tomáš Gonda, Andreas Klingler, Antonio Lorenzin [pdf] [slides]
A Category Theoretic Approach to Approximate Game Theory — Neil Ghani [pdf]
Copy-composition for probabilistic graphical models — Toby St Clere Smithe [pdf] [slides]
Combs, Causality and Contractions in Atomic Markov Categories — Dario Maximilian Stein, Márk Széles [pdf]
Representing Knowledge and Querying Data using Double-Functorial 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 energy-driven systems — Owen Lynch, David Spivak, Matteo Capucci [pdf] [slides]
Compositional statistical mechanics, entropy and variational free energy — Grégoire Sergeant-Perthuis [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 Time-Varying Data — Benjamin Merlin Bumpus, James Fairbanks, Martti Karvonen, Wilmer Leal, Frédéric Simard [pdf]
Overview of progress — Adjoint School [pdf]
Inference on poset-shaped diagrams in the category of Markov kernels — Grégoire Sergeant-Perthuis, 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, Jü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 Higher-Order Probability Theory — Benedikt Peterseim [pdf] [slides]
No-go theorems: Polynomial comonads that do not distribute over distribution monads — Nihil Shah, Amin Karamlou [pdf] [slides]
High schoolers excel at Oxford post-graduate 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 Wang-Mascianica, 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, Boldizsár Poó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 2-categories — Adrian Miranda [pdf] [slides]
Learners are Almost Free Compact Closed — Mitchell Riley [pdf] [slides]
Monoidal Optics are Universal — Matt Earnshaw, James Hefford, Mario Román [pdf] [slides]
Reinforcement Learning in Categorical Cybernetics — Jules Hedges, Riu Rodriguez Sakamoto [pdf] [slides]
A Compositional Framework for First-Order Optimization — Tyler E Hanks, Matthew Klawonn, Matthew Hale, Evan Patterson, James Fairbanks [pdf]
Reverse Faà 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]
Higher-Order DisCoCat (Peirce-Lambek-Montague 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 Non-determinism in Concurrent Calculi: The Eager Way — Bas van den Heuvel, Daniele Nantes-Sobrinho, 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 — Jean-Simon 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 string-to-string 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 Liell-Cock and Sam Staton [pdf] [slides]
A strong nominal semantics for fixed-point constraints — Ali Khan Caires Ribeiro, Maribel Fernandez and Daniele Nantes-Sobrinho [pdf] [slides]
Continuous Domains for Function Spaces Using Spectral Compactification — Amin Farjudian and Achim Jung [pdf] [slides]
Cost-sensitive computational adequacy of higher-order 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]
Two-dimensional 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 Jui-Hsuan Wu [pdf] [slides]