Scottish Programming Languages Seminar

When we run a program we get its output but usually no explanation of where that output came from or why. We propose a method for tracking how inputs affect outputs that treats the problem similarly to automatic differentiation. For each input datum, automatic differentiation computes the forward or reverse derivative at that point. For provenance tracking, we compute for each input a Galois connection that describes how approximations of the input and output relate.

This is joint work with Roly Perera.

Inductive program synthesis algorithms search a space of programs to find one that meets some specification. Enumerating syntax of the target language leads to a very large search space due to the presence of semantic duplicates. Constructing and checking these duplicates is time-consuming for no benefit: we propose enumerating semantics, instead of syntax, so that each object constructed is meaningful. We present NSynC, a proof of concept for our synthesis-by-semantics approach, which searches normal forms of the simply-typed lambda calculus with sums.

Indefinite causal order is a characteristic phenomenon in quantum computation, with examples including the quantum SWITCH and the OCB process. Not all such processes are believed to be physically realizable: while some implementations of the quantum SWITCH have been proposed, the OCB process is suspected to be unrealizable. This difference in realizability is commonly attributed to constraints imposed by physical causality. This talk studies such a causality issue in a higher-order setting, proposing a typed lambda calculus with quantum control and its categorical semantics. Our calculus extends pure quantum computation with higher-order functions and quantum conditional branching, and it is equipped with a type system based on intuitionistic BV logic to enforce causality. We also present a novel model that is closely related to the Caus construction, by which we prove that some physically-unrealizable processes are not definable in our language.

This talk is based on the talk accepted to LICS.

The modal μ-calculus is the logic obtained by adding least and greatest fixed-point quantifiers to modal logic. In this talk, we present an ongoing project on formalising a variant of the modal μ-calculus inside Agda. We use the machinery of indexed containers to handle the fixed points. The result is a proof-relevant, constructive Kripke semantics, where the semantics of a formula P assigns to a world w a "type of witnesses" that P holds at w.

This semantics is as of yet only defined for the strictly positive fragment of μML (i.e., the fragment without negation and implication); we're still working on adding the missing connectives, and we'll discuss some possible directions for incorporating implication.

Metaprograms are programs that generate programs. Staging is a well-known approach to metaprogramming that revolves around stage annotations, which separate the generator from the generated program. Using staging, we can both make compiler optimisations explicit and predictable (e.g. inlining), and enable entirely new optimisation techniques (e.g. runtime specialisation). Staging has been successfully implemented in practical functional languages by projects like MetaOCaml and MacoCaml.

One rightfully expects that well-typed metaprograms don't go wrong. Staging in a pure language with a Hindley-Milner type system features works out well: well-typed metaprograms generate well-typed programs. Unfortunately, OCaml’s combination of side effects and advanced type system features (like generalised algebraic datatypes and first-class modules) breaks down the soundness of obvious staging designs. The key issue is the unsound traversal of type information between stages.

In this talk, I will present ongoing work on a sound design of staging in our OCaml dialect — OxCaml. Taking inspiration from Kovacs, we expand stage annotations to not just expressions, but also types. Likewise, we sketch the staging of kinds and modes, painting a full picture of staging OxCaml with all its features.

Commutative regular expressions describe sets of unordered words, and are used, for example, when building type systems for process calculi. In these applications, an important operation is finding the intersection of two expressions, but no algorithm existed in the literature yet. In this talk I will present the algorithm we recently proposed and formalised in Rocq, where we encode the intersection of two expressions as systems of linear Diophantine equations, and extract from their solution an intersection expression.

I will also present an experimental evaluation of the OCaml-extracted solver using >50,000 random generated regular expressions.

This talk will be based on our paper that was recently accepted at ITP (FLoC 2026).