Fermetures et modules dans les langages concurrents avec contraintes fondés sur la logique linéaire
Institution:
Paris 7Disciplines:
Directors:
Abstract EN:
This thesis studies the internalization in the Linear logic Concurrent Constraint languages (LCC) of a module system without modifying the underlying logic. The languages resulting from this internalization have simple mono-paradigm semantics and embed numerous programming concepts such that non-determinism, constraints, imperative assignment, concurrence, closures et code encapsulation. This great simplicity of this approach allows to obtain directly first-order logical semantics. In the first part of this thesis, we show that the declarations usual in LCC languages can be taken out, to the benefit of a new "persistent ask" agent, while preserving the logical semantics of the language. We also show that the languages resulting from this internalization have all the expressive power of functional languages and usual process calculi. In the second part we define a module system for this class of languages, in which modules can be referenced by variables. We show then than the implementation hiding can be obtained with the usual variable hiding operator. Finally we present a prototype of implementation of one instance of this module system and illustrate its use in logical constraint programming.
Abstract FR:
Cette thèse étudie l'internalisation dans les langages concurrents avec contraintes fondés sur la logique linéaire (LCC) d'un système de modules sans modification de la logique sous-jacente. Il en résulte un langage opérationnellement très simple et mono-paradigme qui incorpore nativement un grand nombre de concepts de programmation tels que le non déterminisme, les contraintes, l'affectation imperative, la gestion de la concurrence, les fermetures et l'encapsulation de code. Cette grande simplicité permet alors d'obtenir de façon directe une sémantique logique premier ordre. Dans la première partie de cette thèse nous montrons que les déclarations de procédures des langages LCC peuvent être supprimées au profit d'un nouveau type d'agent asks persistants tout en préservant la sémantique logique du langage. Nous montrons que le langage qui résulte de cette internalisation des déclarations fournit toute la puissance d'expression des fermetures des langages fonctionnels et des calculs de processus classiques à travers des encodages où les variables jouent le rôle de canaux de communication dynamiques. Dans la seconde partie nous définissons un système de modules pour cette classe de langages, dans lequel les modules peuvent être référencés par des variables. Nous démontrons que, grâce à ce système de modules, le masquage de code s'obtient alors par l'opérateur usuel de masquage des variables. Puis nous présentons un prototype d'implémentation d'une instance de ce système de modules et illustrons son utilisation en programmation avec contraintes.