Rencontre, 27 juin 2024

Programme

10:30 – 12:00

Pierre Clairambault (LIS, Marseille)

Invited talk: An Analysis of Symmetry in Quantitative Semantics

Drawing inspiration from linear logic, quantitative semantics aim at representing quantitative information about programs and their executions: they include the relational model and its numerous extensions, game semantics, and syntactic approaches such as non-idempotent intersection types and the Taylor expansion of lambda-terms. The crucial feature of these models is that programs are interpreted as witnesses which consume bags of resources.

Bags are often taken to be finite multisets, i.e. quotiented structures. Another approach typically seen in categorifications of the relational model is to work with unquotiented structures (e.g. sequences) related with explicit morphisms referred to here as symmetries, which express the exchange of resources. Symmetries are obviously at the core of these categorified models, but we argue their interest reaches beyond those --- notably, symmetry leaks in some non-categorified quantitative models (such as the weighted relational model, or Taylor expansion) under the form of numbers whose combinatorial interpretation is not always clear.

In this work, we build on a recent bicategorical model called thin spans of groupoids. Notably, thin spans feature a decomposition of symmetry into two sub-groupoids of polarized --- positive and negative --- symmetries. We first construct a variation of the original exponential of thin spans, based on sequences rather than families. Then we give a syntactic characterisation of the interpretation of simply-typed lambda-terms in thin spans, in terms of rigid intersection types and rigid resource terms. Finally, we formally relate thin spans with the weighted relational model and generalized species of structure. This allows us to show how some quantities in those models reflect polarized symmetries: in particular we show that the weighted relational model counts witnesses from generalized species of structure, divided by the cardinal of a group of positive symmetries.

This is joint work with Simon Forest.

13:45 – 14:45

Matthieu Piquerez (Galinette, INRIA)

Invited talk: Machine-Checked Categorical Diagrammatic Reasoning

We describe a formal proof library, developed using the Coq proof assistant, designed to assist users in writing correct diagrammatic proofs, for 1-categories. This library proposes a deep-embedded, domain-specific formal language, which features dedicated proof commands to automate the synthesis, and the verification, of the technical parts often eluded in the literature.

Joint work with Benoît Guillemet and Assia Mahboubi, see https://arxiv.org/abs/2402.14485

15:15 – 16:15

Aloÿs Dufour (LIPN, Université Sorbonne Paris-Nord)

Invited talk: Böhm and Taylor for all

Böhm approximations, used in the definition of Böhm trees, are a staple of the semantics of the lambda-calculus. Introduced more recently by Ehrhard and Regnier, Taylor approximations provide a quantitative account of the behavior of programs and are well-known to be connected to intersection types. The key relation between these two notions of approximations is a commutation theorem, roughly stating that Taylor approximations of Böhm trees are the same as Böhm trees of Taylor approximations. Böhm and Taylor approximations are available for several variants or extensions of the lambda-calculus and, in some cases, commutation theorems are known. In this paper, we define Böhm and Taylor approximations and prove the commutation theorem in a very general setting. We also introduce (non-idempotent) intersection types at this level of generality. From this, we show how the commutation theorem and intersection types may be applied to any calculus embedding in a sufficiently nice way into our general calculus. All known Böhm-Taylor commutation theorems, as well as new ones, follow by this uniform construction.

Joint work with Damiano Mazza.