Normal view MARC view ISBD view

Réceptivité, mobilité et pi-calcul / Cédric Lhoussaine ; sous la direction de Roberto Amadio et Gérard Boudol

Auteur principal : Lhoussaine, Cédric, 1974-, AuteurAuteur secondaire : Boudol, Gérard, Directeur de thèse • Amadio, Roberto M., 1963-, Directeur de thèseAuteur secondaire collectivité : Université Aix-Marseille 1, Etablissement de soutenanceType de document : ThèseLangue : français.Pays : France.Éditeur : [S.l.] : [s.n.], 2002Description : 1 vol. (157 p.) ; 30 cmBibliographie : Bibliogr. p. [153]-157.Sujet MSC : 68N18, Theory of software, Functional programming and lambda calculus
97-02, Research exposition (monographs, survey articles) pertaining to mathematics education
12Exx, Field theory and polynomials - General field theory
Note de thèse: Thèse de doctorat, informatique , 2002, université Aix-Marseille IEn-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 LHO (Browse shelf) Available 01652-01

Bibliogr. p. [153]-157

Thèse de doctorat informatique 2002 université Aix-Marseille I

Cette thèse est une contribution au développement de modèles formels décrivant la migration de code. Plus particulièrement, nous y développons un calcul distribué fondé sur un fragment du π-calcul asynchrone dont la syntaxe est enrichie d'une distribution explicite des processus dans des localités et d'un opérateur de migration de processus entre différentes localités. Dans ce modèle, nous prouvons qu'une forme d'absence d'interblocage peut être garantie grâce à un système d'analyse statique simple combiné avec un système de types. Les canaux de communication ont une propriété dite de "réceptivité", et plus généralement nous démontrons la "livrabilité des messages" qui établit que tous les messages émis auront la possibilité d'être reçus, même éventuellement après migration. Une série d'exemples illustrant le "style de programmation réceptif", nous porte à croire que ce calcul distribué reste suffisamment expressif. La réceptivité peut également être exprimée dans le π-calcul asynchrone sans répartition. On démontre dans ce cas que la réceptivité n'est pas obtenue au détriment de son expressivité par un codage "fully-abstract" du π-calcul à récepteurs uniques dans le π-calcul réceptif. Pour cela, nous sommes amenés à développer des techniques de preuves de bisimulations asynchrones "up-to". Enfin, dans la dernière partie de cette thèse nous nous intéressons au problème de l'inférence de types pour le π-calcul réparti. Nous montrons que la présence de types dépendants complique ce problème et nécessite le développement de nouvelles techniques. Nous donnons un algorithme, qui, étant donné un terme du langage retourne les types les plus généraux. Nous montrons que cet algorithme est correct et complet.

There are no comments for this item.

Log in to your account to post a comment.