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