Institut de Mathématiques de Marseille, UMR 7373




Rechercher


Accueil >

Sémantique dénotationnelle de la logique linéaire avec plus petits et plus grands points fixes de types

Jeudi 11 octobre 11:00-12:30 - Thomas EHRHARD - IRIF, Paris 7

Sémantique dénotationnelle de la logique linéaire avec plus petits et plus grands points fixes de types

Résumé : 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.

JPEG - 5.4 ko
Thomas EHRHARD

Lieu : Salle des séminaires 304-306 (3ème étage) - Institut de Mathématiques de Marseille (UMR 7373)
Site Sud - Bâtiment TPR2
Campus de Luminy, Case 907
13288 MARSEILLE Cedex 9

Exporter cet événement

Pour en savoir plus sur cet événement, consultez l'article Séminaire Logique et Interactions