Rencontre, 14 mars 2024

Programme

10:30 – 12:00

Thomas Ehrhard (CNRS, Université Paris Cité)

Invited talk: Intégration dans les cônes

On a utilisé les cônes positifs de Selinger, munis de tests de mesurabilité, pour faire un modèle de la programmation fonctionnelle probabiliste dans un papier de 2018, avec Michele Pagani et Christine Tasson. Dans ce modèle, l'échantillonnage était interprété au moyen d'une intégrale dont l'existence n'était pas toujours garantie (il y en avait assez pour interpréter une version de PCF, mais on n'aurait pas pu interpréter par exemple un langage call-by-value ou call-by-push-value). Dans un travail récent avec Guillaume Geoffroy, on montre comment l'existence systématique d'intégrales peut être axiomatisée très simplement dans une version légèrement modifiée de ces cônes, qui donnent un modèle de la logique linéaire intuitionniste. Ces intégrales sont définies dans le style des intégrales faibles de Pettis. On montre aussi comment la présence de ces intégrales permet de donner au modèle des propriétés très souhaitables qui n'étaient pas disponibles avant.

The talk will be in english upon request

13:45 – 14:45

Luc Pellissier (Université Paris-Est Créteil)

Invited talk: Droit expérimental des algorithmes publics

Les programmes utilisés par les administrations publiques ont des obligations théoriques de transparence et de compréhension par la société. Nous verrons ces droits, comment ils sont appliqués, et ce qu'on peut dire des notions de spécification ou d'algorithme sous-jacentes. Sur l'exemple du programme qui pseudonymise les décisions de justice judiciaire avant mise en ligne, je présenterai une stratégie juridictionnelle pour faire vivre ces droits.

The talk will be in french.

15:15 – 16:15

Rémi di Guardia (LIP, ENS de Lyon)

Invited talk: Retractions in Multiplicative Linear Logic

Given formulas A and B, A is a retraction of B if there exist proofs of A |- B and B |- A which compose to the axiom on A, up to cut-elimination and axiom-expansion. This gives a natural notion of sub-tying, and corresponds to retractions in the category of proofs: objects are formulas, and morphisms proofs up to cut-elimination and axiom-expansion. While isomorphisms for multiplicative linear logic have been characterized (Balat & Di Cosmo gave a corresponding equational theory in 1999), and there is a well-known retraction (which is not an isomorphism), there is not even a conjecture on what the set of retractions could be.

I will present a work in progress about this problem, giving properties showing the problem should not be too hard, then solving the case "an atom X is a retraction of a formula B" using proof nets. Meanwhile, I will also show difficulties for solving the general case, as well as what happens in other fragments of linear logic.