We say type X is searchable if for any given p : X → 2, we can either find x : X with p x = 0 (a root of p), or determine that there is none. The problem addressed in this talk is to construct plenty of searchable infinite types. For this purpose, we take guidance from topology, where searchability corresponds to compactness, with Johnstone’s topological topos taken as our leading interpretation of our type theory. For example, the notion of total separatedness (the clopens separate the points) plays a crucial role, to guarantee that there are enough maps X → 2 and hence the notion of searchability is not vacuous, so that our searchable types get interpreted as Stone spaces (compact totally separated spaces). A first example of an infinite searchable type is that of non-increasing binary sequences, which gets interpreted as the one-point compactification of the discrete natural numbers. When then show that searchable types enjoy many closure properties. All searchable types we are able to construct at present are automatically well-ordered. We construct an interpretation of Brouwer ordinals, or codes, which consist of certain inductively defined countably branching trees, as well-ordered searchable types. We conclude the talk by generalizing this interpretation to an inductive-recursive universe of searchable types, whose codes are ordinal-branching, rather than just countably branching. For the constructive notion of well-ordered type we adopt, it is not the case in general that every non-empty subset has a least element, but this is the case for the complemented subsets of the well-ordered searchable types we construct.

For this special session of MFPS, this talk will give an introduction to the notion of graded logics and graded type systems, and give an overview of some key ideas in their semantics, both denotational and operational varieties. The notion of grading is a general technique providing more fine-grained reasoning by reflecting the structure of proof/typing rules into a system of structured indices; it can be understood as exposing a more intensional view of computation or proofs. Examples abound within computer science, and at its intersection with logic, e.g., type-and-effect systems, coeffect systems, bounded linear logic (BLL) and recent variants, subexponentials, the dependency core calculus (DCC) and variants, and more. But the idea of grading has been around in logic since the early 1970s, with graded logics refining the quantification inherent to the Kripke models of necessity and possibility. Throughout these different approaches, we see different styles in how grading is added to a calculus, sometimes pervasively through the structure of judgments, sometimes in a ‘modal meta language’ style. We explore these varieties and consider how grading is represented and leveraged within semantic models. Along the way we will see some useful general constructions involving (co)presheaves and free models. Lastly, I will give an overview of techniques in the literature for reflecting grading in operational semantics.

Many semantic aspects of a formal language can be defined as structural predicates on its abstract syntax, and much of its metatheory can be understood through the logical properties of these predicates. Typical examples include results such as congruence of bisimilarity, type safety, confluence of evaluation, and termination of reduction. While many general theories have been proposed to study some of these properties — notable examples include mathematical operational semantics and categorical rewriting — a theory accounting for all of them, uniformly and abstractly, independently of specific languages and syntactic structures, is still missing.

In a recent line of research, I have proposed to develop such a theory in the form of an algebra of structural predicates, extending traditional ‘logical algebras’ with operations akin to structural definitions of predicates, such as structural recursion and substitution. The resulting algebras — dubbed syntax relation algebras — prove to be not only extremely natural from a mathematical standpoint, but also axiomatizable in a complete, syntax-independent fashion, thereby enabling a truly abstract and uniform development of language metatheory. While this development has already been successfully carried out for a significant portion of ‘classical’ metatheory, a major question remains: whether the algebraic approach scales to coeffectful notions, such as quantitative rewriting, program distance, and graded and modal typing.

This talk addresses precisely this question. It introduces syntax relation algebras and the algebraization of classical language metatheory, and discusses extensions of this algebraization to coeffectful notions.

Lucassen and Gifford’s seminal work on effect systems introduced effect polymorphism, namely, the universal quantification over effect variables. This form of polymorphism improves the typability and reusability of programs, and this idea has been adopted in effect-system-based programming languages, such as Koka and Effekt. On the other hand, graded monads, which have been proposed as a semantic structure for effect systems, so far account only for monomorphic effect systems. In this talk, we report on ongoing work aimed at accommodating effect variables and effect quantification within the framework of graded monads. Toward this goal, we first reformulate graded monads in a 2-categorical setting, and then instantiate this formulation using the 2-category of fibrations over an algebraic theory of effects. This is joint work with Zachery Casey and Marco Gaboardi.

Probabilistic programming languages have become a powerful tool for modelling complex, uncertain systems—applied across AI, machine learning, robotics, finance, and beyond. Yet reasoning about such programs, particularly those with infinite loops, poses fundamental semantic and computational challenges.

This talk introduces probability generating functions (PGFs) as a semantic foundation for discrete probabilistic programs. PGFs represent full probability distributions exactly. We present a denotational, forward PGF-transformer semantics—a faithful instantiation of Kozen’s seminal semantics—that unlocks a coherent suite of program-analysis techniques.

We provide a syntactic characterisation of programs whose semantics admits rational closed-form PGFs, ensuring algebraic tractability and efficient computation of tail bounds, moments etc. This extends to conditioning—a key asset of probabilistic programming—enabling exact Bayesian inference, even in the presence of diverging loops.

The PGF framework yields a decidability result for checking program equivalence for programs that e.g. produce standard distributions.

Finally, we reflect on occupation invariants–a dual view to martingales that characterises a loop’s expected state-visit counts as a least fixpoint, synthesisable semi-automatically as rational PGFs, and often yielding positive almost-sure termination as a by-product.

Experiments with our software tool Prodigy show the feasibility of these analyses.

Ergo: we show how the classical theory of generating functions provides a surprisingly coherent and computationally effective foundation for exact reasoning about discrete probabilistic programs.​​​​​​​​​​​​​​​​

Algebraic effects are a way to describe and reason about computational effects in a modular way, via the algebraic theories from universal algebra. A current challenge is to extend these ideas to concurrent programming. In this talk, I will present recent work on modelling dynamic thread creation, inspired by POSIX fork, using an algebraic theory. The main result characterizes this algebraic theory in terms of pomsets, a standard concept from concurrency theory. The algebraic theory induces a monad which we use to give denotational semantics for a core concurrent programming language.

This is joint work with Ohad Kammar, Jack Liell-Cock, Sam Lindley, and Sam Staton.

In this talk I will overview and show my view on developments and understanding of coalgebraic semantics, in particular motivated and exemplified on the case of probabilistic transition systems and automata. We will move from bisimilarity, via (an approach to) trace semantics and its axiomatizations, to relaxed simulations and bisimulations and the notion of epsilon bisimilarity and the accompanying distance. Most of the talk will be of introductory and of overview character, with some highlights of more recent results on epsilon distance as well as axiomatizations of (infinite) trace semantics.

The Functional Machine Calculus (FMC) is a new model of higher-order computation with effects. Consisting of a minimal set of elementary instructions that operate a simple stack machine, it nevertheless embeds a wide array of computational phenomena: evaluation mechanisms (call-by-name, call-by-value, Moggi’s computational metalanguage, Levy’s call-by-push-value), effects (higher-order mutable store, input/output, probabilistic choice), and control operations (conditionals, exception handling, and iteration).

In this talk I will use the FMC to make a few observations on the semantics of programming with effects. I believe these to be interesting both in and of themselves and in highlighting similarities and differences between the FMC and related formalisms.

The Wasserstein (a.k.a. Kantorovich) lifting is a standard method for equipping with a metric the collection of probability distributions on a given metric space. It has become, since the early 2000’s, a key technical tool in program semantics for defining behavioral metrics. The Wasserstein lifting has recently been axiomatized in the context of quantitative algebra, by Mardare, Panangaden and Plotkin. In this talk I will discuss an interesting viewpoint on this axiomatization based on the standard notion of convex function from analysis.

I first got to know Alex when I joined the LFCS in Edinburgh in 1991. In this short, mainly non-technical video talk, I will reflect on some of the many things we have shared over the years, both mathematically and otherwise.

I shall advocate modelling probabilistic programs as random-variable transformers, and use this to introduce a simple Hoare-style program logic for reasoning about programs in a simple imperative probabilistic language.

In classical mathematics, there is a single established homotopy theory of ∞-groupoids, presented for instance by Kan simplicial sets. In a constructive metatheory things are less clear. One good candidate is the homotopy theory presented by the constructive Kan–Quillen model structure on simplicial sets. However, this homotopy theory has the classically surprising feature that its 0-truncated objects (or “h-sets”) form a category equivalent not to the original category of sets, but to its ex/lex completion (setoids).

This talk will consider the situation where our original set theory was itself produced by an ex/lex completion. In this case, I will explain how we can modify the constructive Kan–Quillen model structure to avoid a “double ex/lex completion”, by imposing a condition of levelwise projectivity. The motivation is an ongoing project to construct an elementary ∞-topos (with pushouts) whose underlying 1-topos of 0-truncated objects is the effective topos.

I will report on progress in defining Higher Observational Type Theory (HOTT) as a library inside a type theory with internal parametricity (parametric OTT, POTT). In POTT, each type is equipped with a proof-relevant congruence relation which is reflexive. This is called the logical relation or bridge type. Bridge is not a real identity type, as it does not support transport. Inside POTT, we define a subuniverse of fibrant types via a higher coinductive family. Fibrant types support transport, and the bridge for a fibrant type is its identity type. Bridge for the universe of fibrant types corresponds to equivalence providing definitional univalence. We show that fibrant types are closed under 0, 1, Pi, Sigma, indexed W and indexed M. Fibrancy of the universe of fibrant types is still work in progress.

This is joint work with Thorsten Altenkirch, Michael Shulman and Szumi Xie.