Abstracts

• On type inference in the intersection type discipline :
  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 lambda-calculus, where one never erases arguments that would be discarded by ordinary beta-reduction. We show that our notion of unification allows us to compute a principal typing for any strongly normalizing lambda-expression.
  
  
• Récursion généralisée et inférence de types avec intersection:
  In the first part, we define a new programming language with a functional core and generalised recursion, by using Boudol's type system with degrees to rule out unsafe recursions. The language is extended first with recursive records, then with mixins, allowing the programmer to fully mix functional and object-oriented paradigms. We also present an implementation, MlObj, and an abstract machine for execution.
  
  In a second part, we design a new inference algorithm for intersection type systems, on an extension of the lambda-calculus. After proving its correctness, we study its generalisation to references and recursion, we compare it with existing inference algorithms, mainly System I, and we show that its finite rank version becomes decidable.
  
  
• Using ambients to control resources:
  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 reducing the 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 static resource control possible in our setting, and enhance it with a rich notion of resources.
  
  
• Recursion in the call-by-value lambda-calculus:
  We propose an abstract machine to run the call-by-value lambda-calculus extended with a call-by-value fixed-point, and we show that this provides us with a correct implementation of our calculus.
  
  
• On the expressiveness of pure mobile ambients:
  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, and 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.
  
  
• Subtyping and typing algorithms for mobile ambients:
  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.