19/10/2000: Thomas Ehrhard, IML Marseille---
Espaces de Köthe et logique linéaire.
Résumé
Une notion standard de la théorie des espaces vectoriels
topologiques (les "espaces de suites de Köthe") peut être utilisée
pour construire un modèle dénotationnel de la logique linéaire
où les formules sont interprétées par des espaces vectoriels
topologiques localement convexes (séparés, séparables, complets)
et les preuves par des fonctions linéaires continues. Dans le
modèle du lambda-calcul simplement typé qui est associé à
cette sémantique de la logique linéaire (la "catégorie de
Kleisli de la co-monade '!'", qui est cartésienne fermée), les
morphismes sont des fonctions analytiques définies partout.