In order to answer the challenge of pervasive computing, we propose a new process calculus, whose aim is to describe dynamic systems composed of agents able to move and react differently depending on their location. This Context-Aware Calculus features a hierarchical structure similar to mobile ambients, and a generic multi-agent synchronization mechanism, inspired from the join-calculus. After general ideas and introduction, we review the full calculus' syntax and semantics, as well as some motivating examples, study its expressiveness, and show how the notion of computation itself can be made context-dependent.

We introduce a new unification procedure for the type inference problem in the intersection type discipline. We show that unification exactly corresponds to reduction in an extended λ-calculus, where one never erases arguments that would be discarded by ordinary β-reduction. We show that our notion of unification allows us to compute a principal typing for any strongly normalizing λ-expression.

Dans une premiere partie, nous definissons un nouveau langage a base fonctionnelle et avec recursion generalisee, en utilisant le systeme de types avec degres de Boudol pour eliminer les recursions dangereuses. Ce langage est ensuite etendu par des enregistrements recursifs, puis par des mixins, permettant ainsi de meler totalement les paradigmes fonctionnels et objets. Nous presentons egalement une implementation, MlObj, ainsi que la machine abstraite servant a son execution. Dans une deuxieme partie, nous presentons un nouvel algorithme d'inference pour les systemes de types avec intersection, dans le cadre d'une extension du lambda-calcul. Apres avoir prouve sa correction, nous etudions sa generalisation aux references et a la recursion, nous le comparons aux algorithmes d'inference deja existants, notamment a celui de Systeme I, et nous montrons qu'il devient decidable a rang fini.

We consider the Pure Safe Ambient Calculus, which is Levi and Sangiorgi's Safe Ambient Calculus (a variant of Cardelli and Gordon's Mobile Ambient Calculus) restricted to its mobility primitives – in particular, we focus on its expressive power. Since it has no form of communication or substitution, we show how these notions can be simulated by mobility and modifications in the hierarchical structure of ambients. As a main result, we use these techniques to design an encoding of the synchronous $\pi$-calculus into pure ambients, and we study its correctness, thus showing that pure ambients are as expressive as the $\pi$-calculus. In order to simplify the proof and give an intuitive understanding of the encoding, we design an intermediate language, the $\pi$-Calculus with Explicit Substitutions and Channels, which is an extension of the $\pi$-calculus in which communication and substitution are broken into simpler steps, and we show that is has the same expressive power as the $\pi$-calculus.

Current software and hardware systems, being parallel and reconfigurable, raise new safety and reliability problems, and the resolution of these problems requires new methods. Numerous proposals attempt at reducingthe threat of bugs and preventing several kinds of attacks. In this paper, we develop an extension of the calculus of Mobile Ambients, named Controlled Ambients, that is suited for expressing such issues, specifically Denial of Service attacks. We present a type system for Controlled Ambients, which makes resource control possible in our setting.

The ambient calculus was designed to model mobile processes and study their properties. A first type system was proposed by Cardelli-Gordon-Ghelli to prevent run-time faults. We extend it by introducing subtyping and present a type-checking algorithm which returns a minimal type relatively to this system. By the way, we also add two new constructs to the language. Finally, we remove the type annotations from the syntax and give a type-inference algorithm for the original type system.

We introduce a new unification procedure for the type inference problem in the intersection type discipline. We show that unification exactly corresponds to reduction in an extended - calculus, where one never erases arguments that would be discarded by ordinary -reduction. We show that our notion of unification allows us to compute a principal typing for any strongly normalizing -expression.