Rencontre, 25 janvier 2024

Programme

10:30 – 12:00

Emmanuel Beffara (Univ. Grenoble Alpes)

Invited talk: Concurrent Realizability on Conjunctive Structures

This work aims at exploring the algebraic structure of concurrent processes and their behavior independently of a particular formalism used to define them. We propose a new algebraic structure called conjunctive involutive monoidal algebra (CIMA) as a basis for an algebraic presentation of concurrent realizability, following ideas of the algebrization program already developed in the realm of classical and intuitionistic realizability. In particular, we show how any CIMA provides a sound interpretation of multiplicative linear logic. This new structure involves, in addition to the tensor and the orthogonal map, a parallel composition. We define a reference model of this structure as induced by a standard process calculus and we use this model to prove that parallel composition cannot be defined from the conjunctive structure alone.

This is joint work with Félix Castro, Mauricio Guillermo and Étienne Miquey

13:45 – 14:45

Gabriel Scherer (Parsifal, INRIA)

Invited talk: Constructor unboxing

In this work I will present a new feature proposed for the OCaml programming language, “constructor unboxing”, first suggested by Jeremy Yallop in March 2020. It enables a more efficient representation of certain sum types, but requires a static analysis to forbid certain unboxing requests that would be unsound.

To define this static analysis, one has to solve a problem of normalization of first-order definitions in presence of recursion. In the talk I hope to explain my current understanding of this halting problem, and present an algorithm to compute normal forms and reject (in finite time) non-normalizable definitions.

15:15 – 16:15

Marie Kerjean (LIPN, Université Sorbonne Paris-Nord)

Invited talk: DiLL est dans Laplace

What do exponential maps and exponential connectives have in common? Well, more than we thought! This talk will describe several way in which they interact.

First, we will see how the exponential map helps construct the differentiation monad, a variant of the continuation monad where the unit is the differential. This monad has the nice property of characterizing quantitative programs, equal to their Taylor expansion.

We will also see how the exponential map gives a good interpretation of the co-digging, a fourth co-structural exponential rule missing to those added by Differential Linear Logic to Linear Logic. If time permits, we will look at its nice graded properties.

Finally, we will see how the exponential function defines the Laplace transformation, which transforms exponential connectives by turning distributions of type "!" into functions of type "?". We will see how this Laplace transformation turns co-structural rules into structural ones and explore its beautiful categorical properties.

This is joint work with Jean-Simon Pacaud Lemay.