Thomas Ehrhard
IRIF, Université de Paris
https://www.irif.fr/~ehrhard/
Date(s) : 11/10/2018 iCal
11 h 00 min - 12 h 30 min
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