Many logics used in computer science manipulate propositions about systems in different states.

There are resource dependent logics, where the resources in a state can be ‘shared’ or ‘not shared’. Accordingly, there are two conjunctions for propositions – one for when the conjunction can be proved when sharing resources, and one for non-shared resources.

Then there are temporal logics for reasoning about systems evolving through discrete time, where our logical calculus is augmented with connectives about what will happen in the future, after a discrete time jump.

Separation logic was developed to reason about programs running in the standard execution model involving pointers and heaps (i.e. mutable data structures). Heaps can be combined, but only if they are ‘disjoint’, so as to avoid an extra condition of consistency on their intersection which helps with reasoning at scale. Separation logic introduces a ‘separating conjunction’ that expresses that the propositions involved are satisfied on disjoint parts of the heap.

In all these examples, structure on the set of states is being lifted to the propositions about those states. In this talk, we will discuss how that lifting is calculated by using a generalisation of a classical category-theoretic construction: Day convolution. This ‘extension construction’ lifts all (partial) algebraic structure on the set of states to logical operations on the propositions about those states.
Moreover, the extended operations are automatically residuated, meaning they admit a notion of implication.

This is joint work with Edmund Robinson.

Relevant paper: Edmund Robinson and Joshua Wrigley. "Day algebras." arXiv:2504.06200 (2025).