TypiCal

Résumé: Les espaces de finitude forment une sémantique dénotationnelle de la logique linéaire dont les formules sont interprétées par des espaces vectoriels topologiques et les preuves par par des applications linéaires continues. En étudiant la topologie des espaces de finitude, nous avons défini une notion algébrique de totalité qui permet de définir un modèle de la logique linéaire plus fin que celui des espaces de finitude. Ainsi, nous avons obtenu un théorème de complétude pour un lambda-calcul avec une somme barycentrique et des constructions booléennes au premier ordre.

Cet exposé débutera par l'étude d'un lambda-calcul barycentrique booléen. Après en avoir introduit un modèle utilisant des polynômes, je présenterai un théorème de complétude pour ce calcul. Dans un second temps, je définirai les espaces de finitude et la totalité qui nous ont amenés à considérer ce théorème.

Liens: la page personnelle de l'intervenant, les transparents de l'exposé