Sur la notion d'observation en sémantique
Institution:
Paris 7Disciplines:
Directors:
Abstract EN:
This thesis explores several aspects of the notion of observability in the semantics of programming languages, and its applications to relative definability and adequacy of the denotational models of programming languages. In a first part, we show, on the one hand, that the hierarchy of extensional models of PCF is trivial (Scott model and fully abstract model) but th hierarchy of relative defmability is complex, and that relative definability in finitary PCF is an NP-complete problem. The second part gives a model for a programming language with dynamic allocation using FM-cpos. Instrumented with state types and accessibility maps, it allows thé proof of new observational equivalences between programs, such as the "garbage collection" rule. The last part gives a categorical framework to build denotationel semantics that show the length of the computation, measured as a number of clock ticks. The examples of coherence spaces with multicliques and game semantics are examined.
Abstract FR:
Cette thèse explore plusieurs facettes de la notion d'observabilité en sémantique des langages de programmation, et ses applications en matière de définissabilité relative et d'adéquation des modèles dénotationnels des langages de programmation. Dans une première partie, nous montrons que la hiérarchie des modèles extensionnels de PCF unaire est triviale (modèle de Scott et modèle complètement adéquats seulement) mais que la hiérarchie des degrés de défmissabilité est complexe, et que la définissabilité relative dans PCF finitain est un problème NP-complet. La deuxième partie propose un modèle d'un langage de programmation avec allocation dynamique à base de FM-cpos. Le modèle, instrumenté avec des types d'état et des fonctions d'accès ;ssibilité, permet de prouver des équivalences observationnelles entre programmes nouvelles, par exemple, la règle de « garbage collection ». La dernière partie propose un cadre catégorique pour construire des sémantiques dénotationnelles qui représente la longueur du calcul, mesurée par un nombre de « tics » d'horloge. Les exemples des espaces de cohérences munis des multicliques et de la sémantique des jeux sont examinés.