Séminaire, 20 novembre 2025

Programme

10:30 – 11:45

Sonia Marin (University of Birmingham (UK))

Invited talk: Intuitionistic modal logics and their justifications

Justification logic is an explication of modal logic: boxes are replaced with proof terms formally through realisation theorems. In intuitionistic modal logic, boxes and diamonds are decoupled and not De Morgan dual. We propose justification counterparts to some intuitionistic modal logics by making diamonds explicit and introducing new terms called satisfiers. In this talk, we will hopefully introduce enough background information to eventually present an axiomatisation of these justification logics with a syntactic realisation procedure using cut-free (nested) sequent systems for intuitionistic modal logics.

(This is joint work with Paaras Padhiar, building up on other works with Anupam Das and with Roman Kuznets and Lutz Straßburger.)

13:45 – 14:45

Aymeric Walch (ISAE-Supaero)

Invited talk: A compositional approach to Taylor expansion

The combination of the theory of differential calculus with the theory of programming languages is an active field of research, with the development of automated differentiation and of the differential lambda calculus. It is well known that differentiation can be turned into a compositional operation, using the tangent bundle construction, also called dual numbers in automated differentiation.

In this talk, we explain how Taylor expansion at any order can be similarly turned into a compositional operation, using an idea similar to that of jet bundles that appear in differential geometry.

We will then discuss how category theory is a nice framework to describe those ideas. Formally, Taylor expansion is captured as a functor, and the axioms of differential calculus boil down to naturality equations that turns this functor into a monad. This categorical structure is similar to the structure of higher order dual numbers that have found recent applications in automated differentiation.

The first half of this talk does not require prior knowledge on category theory.

15:15 – 16:15

Joshua Wrigley (Université Paris Cité)

Invited talk: Day algebras

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).