Session type : semantic foundations and object-oriented applications
Institution:
Paris 7Disciplines:
Directors:
Abstract EN:
Two processes willing to safely exchange messages must agree on a protocol to adopt during the interaction, to be guaranteed that the communication proceeds without mismatches. In the theory of session types the specification of the protocol is a type associated to the communication channel, that describes the sequence and the direction of exchanged data. In this thesis we study session types both from a foundational perspective and from a linguistic one. We first define a semantics for session types. Since session types are intended to describe the communication behavior of a process, it seems natural for them to be defined not syntactically, following the syntax of the process they describe, but semantically, capturing the observable behavior of processes in terms of the input/output actions they perform. We do this exploiting well-known theories, like set theory and process algebra. We interpret types as sets and define subtyping as the standard set inclusion relation. From process algebra we borrow the concepts of internal and externaJ choices, and we define a reduction semantics for descriptors using standard LTS. On the other side, from a linguistic perspective, we study the design of object-oriented calculi with sessions, which is the first step to the embedding of session types in real languages. The wide adoption of object-oriented paradigm for writing modem applications is the reason that motivates the research efforts towards integrating session-oriented programming with object-oriented programming. We show how to enrich the session types for object-oriented languages with useful features like bounded polymorphism, unions, and parametric polymorphism.
Abstract FR:
Deux processus qui échangent des messages doivent s'accorder sur un protocole à adopter lors de l'interaction, pour avoir la garantie que la communication avance sans discordances. Dans la théorie des types session la spécification du protocole est un type associé au canal et décrit la séquence et la direction des données échangées. Dans cette thèse nous étudions les types session dans une perspective fondatrice et une linguistique. Nous définissons d'abord une sémantique pour les types session. Puisque ces types décrivent le comportement de communication d'un processus, il semble naturel de les définir non pas syntaxiquement, en suivant la syntaxe du processus, mais sémantiquement, en capturant le comportement observable des processus en termes des actions input/output qu'ils effectuent. Nous exploitons des théories bien connues: la théorie des ensembles ; et l'algèbre de processus. Nous interprétons les types comme des ensembles et le sous-typage comme la relation standard d'inclusion. De l'algèbre ; de processus nous empruntons les notions de choix interne et externe et définissons une sémantique de réduction pour les types en utilisant les LTS standard. D'un point de vue linguistique, nous étudions le dessein de calculs orientées objet avec les sessions, qui est la première étape de l'intégration de ces types dans des langages réels. La large adoption du paradigme orienté objet pour écrire des applications modernes est la raison qui motive les efforts de recherche vers l'intégration des paradigmes orientées session et orientées objet. Nous enrichissons les types session pour les langages objet avec le polymorphisme limitées, les unions et le polymorphisme paramétrique.