2026-03-06

Kleene algebra (KA) is an important tool for reasoning about general program equivalences, with a decidable and complete equational theory. However, KA cannot always prove equivalences between specific programs. For this purpose, one adds hypotheses to KA that encode program-specific knowledge. Traditionally, a map on regular expressions called a reduction then lets us lift decidability and completeness to these more expressive systems. Explicitly constructing such a reduction requires significant labour. Moreover, due to regularity constraints, a reduction may not exist for all combinations of expression and hypothesis.

We describe an automaton-based construction to mechanically derive reductions for a wide class of hypotheses. These reductions can be partial, in which case they yield partial completeness: completeness for expressions in their domain. This allows us to automatically establish the provability of more equivalences than what is covered in existing work.

Separation logic enables modular reasoning about programs by treating memory as a splittable resource. Its principle idea is that programs operate on small, local parts of memory, allowing reasoning to be confined to those parts. Variants of this idea have been developed for concurrency, permissions, and probabilistic resources, each tailored to a particular resource structure.

This raises a natural question: can separation logics be derived systematically from a given notion of resource, rather than designed case by case?

In this talk I present a categorical framework in which separation logic arises from first-order logic made resource-aware. Predicates are defined internally in a category of sheaves, which model local views on resources and their gluing. Separating conjunction then emerges from the way resources combine.

As a concrete example, I construct the logic induced by a memory sheaf with finite support and derive the semantics of separating conjunction. I then outline how varying the underlying sheaf changes the resulting logic, giving separation logics for different resource models.

Session Typed π-calculus, in various forms, has been proposed as a programming language corresponding, under Curry-Howard, to sequent calculus presentation of (intuitionistic) linear logic. This correspondence has been studied from various perspectives, establishing tight connection between the dynamics of processes and proofs, and techniques like logical relations have been developed to study properties of the processes.

In comparison with the Curry-Howard story for λ-calculus, one area that did not receive a lot of attention is the study of models. In this talk we report on some steps taken in that direction.

Specifically, we consider a class of models for session typed π-calculus that arise from Petri Nets. Existing work on linear logic demonstrated how linear logic can be used to talk about reachability in a Petri Net. We extend this class of models to π-calculus, allowing us to express not only whether a certain marking is reachable in a Petri Net, but how it can be reached.