Sémantique dénotationnelle de la logique linéaire avec plus petits et plus grands points fixes de types
Thomas Ehrhard
IRIF, Université de Paris
https://www.irif.fr/~ehrhard/
Date(s) : 11/10/2018 iCal
11h00 - 12h30
On montrera comment interpréter μLL – la logique linéaire propositionnelle avec plus petits (μ) et plus grands (ν) points fixes de types – dans les espaces cohérents, puis dans les espaces cohérents avec totalité. Le premier modèle ne fait pas la différence entre μ et ν, alors que le second, bâti sur le premier, interprète μ et ν de façons différentes. La même technique s’adapte à beaucoup d’autres modèles, et notamment aux espaces de finitude. μLL peut être vu comme un langage de programmation fortement normalisant contenant le système T de Gödel et permettant de définir de nombreux “types de données” (listes, arbres, mais aussi streams etc).
Travail en collaboration avec Farzad Jafrrahmani.
Catégories Pas de Catégories
