Rencontre, 12 mars 2026

Programme

10:30 – 11:45

Jean Krivine (CNRS, IRIF)

Invited talk: Reversible Computations are Computations

Causality serves as an abstract notion of time for concurrent systems. A computation is causal, or simply valid, if each observation of a computation event is preceded by the observation of its causes. The present work establishes that this simple requirement is equally relevant when the occurrence of an event is invertible. We propose a conservative extension of causal models for concurrency that accommodates reversible computations. We first model reversible computations using a symmetric residuation operation in the general model of configuration structures. We show that stable configuration structures, which correspond to prime algebraic domains, remain stable under the action of this residuation. We then derive a semantics of reversible computations for prime event structures, which is shown to coincide with a switch operation that dualizes conflict and causality.

This is joint work with Clément Aubert, Augusta University. USA.

Reference https://www.coalg.org/calco-mfps-2025/pre-proceedings/MFPS25-29.pdf

13:45 – 14:45

Éléonore Mangel (IRIF)

Invited talk: Classical notions of computation and the Hasegawa-Thielecke theorem

In the spirit of the Curry-Howard correspondence between proofs and programs, we define and study a syntax and semantics for classical logic equipped with a computationally involutive negation, using a polarised effect calculus, the linear classical L-calculus. A main challenge in designing a denotational semantics for the calculus is to accommodate both call-by-value and call-by-name evaluation strategies, which leads to a failure of associativity of composition. In order to tackle this issue, we define a notion of adjunction between graph morphisms on non-associative categories, which we use to formulate polarized and non-associative notions of symmetric monoidal closed duploid and of dialogue duploid. We show that they provide a direct style counterpart to adjunction models: linear effect adjunctions for the (linear) call-by-push-value calculus and dialogue chiralities for linear continuations, respectively. In particular, we show that the syntax of the linear classical L-calculus can be interpreted in any dialogue duploid, and that it defines in fact a syntactic dialogue duploid. As an application, we establish, by semantic as well as syntactic means, the Hasegawa-Thielecke theorem, which states that the notions of central map and of thunkable map coincide in any dialogue duploid (in particular, for any double negation monad on a symmetric monoidal category).

This is joint work with Paul-André Melliès and Guillaume Munch-Maccagnoni

15:15 – 16:15

Davide Barbarossa (LIP, ENS de Lyon)

Invited talk: Computational interpretations of logic : the case of Dialectica

I will first recall some computational interpretations of logic, with a focus on Gödel's Dialectica -- which plays a central role in concrete applications of proof theory to mainstream mathematics via the so-called "proof mining" program.

Then I will discuss some content from a recent joint work with Thomas Powell (University of Bath): we present Dialectica as a collection of rules inspired by Hoare logic ; in this way, Dialectica is viewed as a specification system for "procedural" programs that come with a forward and backward direction, and this viewpoint naturally captures the dynamics of extracted realisers from proofs. We also define a big-step semantics for (a fragment of) this system, that shows that Dialectica performs a generalised backpropagation.