ABSTRACT. When does the order of elements "not matter" in a random sequence? The notion of exchangeability formalizes this idea as a symmetry property of a distribution. While seemingly abstract, exchangeability has been the subject of deep theoretical study and is a fundamental assumption in a variety of practical applications, enabling statistical hypothesis tests and conformal prediction. However, formal verification of exchangeability appears challenging, and has received little study. In this talk, I'll present some of our recent work on type systems for finite exchangeability. Following a common theme in programming languages, rather than tackling exchangeability directly, we focus on transformations that preserve this property. Inspired by research on bidirectional programming, we propose a new notion of equivariant lens and show that these morphisms preserve a generalization of exchangeability. By leveraging the rich categorical structure of these lenses, we develop two new type systems for building exchangeability preserving transformations and exchangeable distributions. Joint work with Vaibhav Mehta (Cornell).

ABSTRACT. Simulation and bisimulation play a central role in coalgebra and in program semantics. Bisimulation is a certain canonical notion of program (or system) equivalence, which can be formulated in different equivalent ways in base cases, while these ways need not remain equivalent under further generalizations. This is acknowledged and investigated in the literature. Contrastingly, simulation is a non-canonical notion of program in-equivalence (or approximation), subject to the same issue, but much less explored. This is a work in progress on exploring it.

ABSTRACT. We propose a framework for compositional verification of higher-order effectful programs based on operational game semantics. Starting from a monadic evaluator for a programming language, the framework derives interactive models of open program components as monadic transducers indexed by games. Their composition is defined by a bidirectionnal synchronization process based on feedback loops, in the style of Geometry of Interaction, and expressed algebraically through a trace operator induced by monadic iteration. This provides a common structure for approximating both evaluation and composition, opening the way to abstract-interpretation techniques for computing or over-approximating the behaviour of composed components. The approach is illustrated by ongoing implementation work in the CAVOC project for OCaml modules.

ABSTRACT. Many verification techniques rely on lifting a system signature from a category of state spaces to a category of predicates, relations, metrics, or other proof objects. Codensity lifting provides a general method for constructing such liftings and has led to applications in fibrational bisimulation, quantitative reasoning, modal logics, and compositional verification. However, the literature often introduces new categorical machinery for each particular instance, making it difficult to identify the general structure that explains why these constructions work. This talk presents work in progress towards a 2-categorical account of codensity lifting. The aim is to separate the formal part of the construction from the application-specific verification data. From this perspective, several existing results on codensity lifting arise as instances of general fibrational and 2-categorical principles.

ABSTRACT. We present a parameterised algebraic theory for classically controlled quantum communication, together with two sound models -- a quantum-stream-based operational semantics and a monadic denotational semantics. The two models induce the same notion of program equivalence -- the denotational one is adequate and fully abstract with respect to the operational one. We view this as a first step towards equational verification of quantum communication protocols.

ABSTRACT. We present a novel abstract interpretation-based static analysis framework for proving Termination Resilience, the absence of Robust Non-Termination vulnerabilities in software systems. Robust Non-Termination characterizes programs where an untrusted (e.g., externally-controlled) input can force infinite execution, independently of other trusted (e.g., internally-controlled) variables. Our framework is a semantic generalization of Cousot and Cousot’s abstract interpretation-based ranking function derivation, and our sound static analysis extends Urban and Miné’s decision tree abstract domain in a non-trivial way to manage the distinction between untrusted and trusted program variables. The talk concludes with open challenges in dealing with angelic non-determinism, pointer-manipulating programs, and going beyond termination to program properties expressed in Computational Tree Logic (CTL) or Alternating-Time Temporal Logic (ATL).

ABSTRACT. 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 labelled partial orders, leading to a semantics where concurrent programs denote partial orders. The algebraic theory provides sound and complete equational reasoning principles for equality of such partial orders. This is joint work with Ohad Kammar, Jack Liell-Cock, Sam Lindley, and Sam Staton.

ABSTRACT. Fixpoints play a central role throughout computer science, and classical fixpoint theory provides fundamental tools for establishing their existence and analyzing the convergence of fixpoint iterations. At the same time, in modern computer science, there has long been a trend to consider classical problems in approximative settings, such as quantitative problems in which the true dynamics of an underlying system cannot be known precisely but may be approximated. Reinforcement learning is a prominent example: optimal policies can be derived from fixpoints of operators whose dynamics are typically unknown and must be learned through interaction with an environment. Despite the growing importance of reinforcement learning, the fixpoint-theoretic foundations of such approximative settings remain comparatively underdeveloped. Approximative fixpoint theory seeks to address this gap by studying fixpoint computation when the operator of interest is accessible only through a sequence of approximating functions converging to it. In this framework, standard fixpoint iteration may fail to converge to a fixpoint, even when its classical assumptions are satisfied, necessitating new techniques and proof methods. In this talk, I will introduce the basic concepts of approximative fixpoint theory and discuss convergence results of the so-called dampened Mann iteration. As an application, these results yield generalized convergence guarantees for (model-based) reinforcement learning algorithms and provide a step towards a unifying fixpoint-theoretic perspective on quantitative learning in environments with unknown dynamics.

ABSTRACT. I will exhibit very simple problems of safety and reachability verification, and several fixed point algorithm for them. These simple problems, however, expose subtle yet fundamental issues on fixed points in model checking. I will introduce some basic lattice-theoretic results (the Knaster-Tarski, Cousot-Cousot, and Kleene theorems) and constructs (involution, adjoint) and address those issues.