TypiCal

Les espaces cohérents probabilistes ont été introduits par Jean-Yves Girard dans son article sur les espaces cohérents quantiques. Nous reprenons et raffinons un peu sa définition, et nous montrons que ces objets fournissent un modèle de la logique linéaire au complet. Nous montrons qu'ils permettent aussi d'interpréter, sans faire appel aux powerdomains, une version probabiliste du langage fonctionnel PCF et prouvons une version probabiliste du théorème d'adéquation de Plotkin pour ce langage, dont la sémantique opérationnelle est décrite par une matrice stochastique infinie. Enfin, nous décrivons un modèle probabiliste du lambda-calcul pur dans les espaces cohérents probabilistes. Il s'agit d'un travail commun avec Vincent Danos.