Normal view MARC view ISBD view

Approches dynamiques en sémantique de la logique linéaire : jeux et géométrie de l'interaction / Patrick Baillot ; sous la direction de Jean-Yves Girard

Auteur principal : Baillot, Patrick, 1972-, AuteurAuteur secondaire : Girard, Jean-Yves, 1947-, Directeur de thèseAuteur secondaire collectivité : Université d'Aix-Marseille II, 1969-2011, Etablissement de soutenanceType de document : ThèseLangue : français ; anglais.Pays : France.Éditeur : [S.l.] : [s.n.], 1999Description : 1 vol. (140 p.) : fig. ; 30 cmBibliographie : Bibliogr. p. 135-137. Index.Sujet MSC : 03F05, Proof theory and constructive mathematics, Cut-elimination and normal-form theorems
18M05, Monoidal categories and operads, Monoidal categories, symmetric monoidal categories
68Q55, Theory of computing, Semantics in the theory of computing
91A40, Game theory, Other game-theoretic models
97-02, Research exposition (monographs, survey articles) pertaining to mathematics education
Note de thèse: Thèse de doctorat, mathématiques discrètes et fondements de l'informatique, 1999, Aix-Marseille 2En-ligne : Site de l'auteur
Tags from this library: No tags from this library for this title. Log in to add tags.
Current location Call number Status Date due Barcode
CMI
Salle S
Thèses BAI (Browse shelf) Available 00045-01

Bibliogr. p. 135-137. Index

Thèse de doctorat mathématiques discrètes et fondements de l'informatique 1999 Aix-Marseille 2

Cette thèse concerne le calcul, sous la forme de la normalisation des preuves de la logique linéaire. Elle vise à explorer les liens entre trois domaines de la théorie de la démonstration. La sémantique dénotationnelle interprète les preuves par des invariants extensionnels de la normalisation. La géométrie de l'interaction (GdI) décrit les preuves comme des objets communiquant et le calcul comme un flot d'information (l'exécution) circulant entre ces objets. La sémantique des jeux occupe une position intermédiaire : les preuves sont des stratégies qui admettent une description extensionnelle à la manière de la sémantique dénotationnelle, mais également dynamique à la manière de la GdI. Nous donnons une nouvelle preuve de définissabilité pour le modèle de Hyland-Ong de la logique linéaire multiplicative utilisant le critère de correction des longs voyages pour les réseaux. Nous associons ensuite une application à tout réseau multiplicatif exponentiel ; cette application permet de calculer l'interprétation d'une preuve intuitionniste (IMELL) dans le modèle d'Abramsky-Jagadeesan-Malacaria. Nous définissons un modèle de jeux (modèle des stratégies saturées) pour la logique linéaire classique (MELL) et étudions ses liens avec la GdI. Nous le comparons ensuite à des modèles dénotationnels en décrivant un (pseudo-)foncteur d'oubli du temps de ce modèle vers une variante du modèle relationnel : le modèle des relations pointées. Deux raffinements de ce dernier modèle sont étudiés : les espaces de positions bipolarisées et les ordres polarisés ; pour chacun nous établissons des liens précis avec le modèle de jeux. La dernière partie aborde le problème des bornes de complexité en GdI : nous introduisons un modèle de clauses permettant l'interprétation de la logique linéaire élémentaire et définissons une variante de l'exécution terminant en temps élémentaire

There are no comments for this item.

Log in to your account to post a comment.