People

Type systems

Nobuko Yoshida is one of the first to propose process types for a distributed calculus where channels could carry processes.

Didier Remy introduced row types for records, and proposed a type inference for it.

Francois Pottier taught me λ-calculus and type systems, and writes really interesting papers requiring some aspirin for its readers.

Distributed Calculi

Robin Milner developped the π-calculus which is one of the most famous distributed calculus.

Alan Schmitt defined with Jean-Bernard Stefani the M-calculus and the Kell-calculus, which are the basis for my work.

Bibliography

• Oz/K: a kernel language for component-based open programming
  [pdf] [bib]
• Typing communicating component assemblages
  [pdf] [bib]
• Typing Component-Based Communication Systems
  [pdf] [bib]

I am currently working on two parallel subjects:

• Type systems for distributed calculi. A first type system was presented for the Dream framework, whose principal property is to uses records which can be routed as messages. This type sytem merges the type system for records defined by Remy, and the process types defined by Yoshida. The technical report on this topic will soon be available. A first version, with some material lacking, is available here.
• Calculi designed for open programming. We presented a programming language, Oz/K, based on Oz. We indeed added kells and gates to this language, to enable explicit modularity and security. With such a constructs, we can have code mobility, sand-boxes and also sharing.

Ideally, these two subjects will meet when I will be able to find a satisfactory calculus, and a type system for it.

Presentation

Types and type systems

A type system is a formal tool to check if some given program has error or not. Such type system associate a type to any valid program, this type approximating the program execution. For instance, any integer in Java is annotated with the type int. Using such types, the type system can then ensure that every function's parameters are valid, and every structure is manipulated in accordance with its specification.

At first, the programs were totally sequential, and, with the type systems usually used in programming languages, everything was fine. But now, many errors occur because programs are distributed. Problems during communications, causing dead-locks, ...
An even more problematic feature of programs nowadays is the code mobility. Programs can change during execution, and most type system cannot deal with such dynamicity.

My work is to find a type system which would capture communication and code mobility errors. A first study have been done on Dream. From our abstract point of view, Dream defines distributed programs structured in components, which exchange messages on channels. These messages are modifiable structures (called records). We defined a type system for this framework, along with the definition of several of its properties. We now need to implement this type system.

The interest of this first work was to find where the problems were in the definition of type system for distributed languages. My next research in this field would be to study code mobility, and how it interacts with type systems. The goal of this new work is to define and/or extend the dream type system for code mobility.

Distributed calculus

A calculus is a programming language, with very few constants and operator. For instance, the λ-calculus has only three constructs: variables, abstraction and application. Such languages are interesting to study program properties and type systems. In our case, we want to study distributed programs in an open programming context, and specifically, how we can easily program and type them.
A distributed program raises many issues difficult to solve:

• Security. The different parts of the program communicates between each other. It is thus necessary to be able to isolate critical parts from suspect ones, to ensure that no one would be able to cause a failure of the program.
• Achitecture. Distributed programs are generally huge, and need some structuration during their conception and implementation to be understandable and with a minimum number of bugs.
• Dynamic binding. As we saw, distributed programs evolve during execution. For instance, some services can fail: the clients should be able to reconnect to another server giving the same services.
• Dynamic reconfiguration. Distributed programs are often services made available for clients to use them. But in the case the number of clients raises too much, the service must be moved to a faster computer, or duplicated. Dynamic reconfiguration stands for the possibility to move such service, without stopping the program.

To express every constructions in a simple manner is ver difficult and many work proposed until now fail to entierly capture every operations. For instance, we addressed the problem by proposing Oz/K, a programming language based on Oz. But this work is still not satisfactory.
My current work is to study why it is so difficult to define such a calculus, and then propose some motivated solutions.