Research Topics
 System Support
Contact/Visit us

Job opportunities

If you are interested in an internship, a PhD, or a postdoc in the Kell calculus, please contact Alan Schmitt.

The Kell Calculus

Research on the Kell includes four main topics.

Journal papers

Conference and Workshop Papers

Technical Reports

The OzK language

Programming in a distributed and open environment remains challenging because it requires combining modularity, security, concurrency, distribution, and dynamicity. This has lead recently to interesting programming language developments such as Alice, Acute, Oz, JoCaml, ArchJava, etc. However the combination of all the above features with dynamicity, i.e. the ability to build and modify systems during execution, still remains an open question. In the Oz/K language, we study and propose an approach to open distributed programming that exploits the notion of locality, which has been studied intensively during the last decade, with the development of several process calculi with localities, including e.g. Mobile Ambients, Dπ, and Seal. We suggest to use the locality concept as a general form of component, that can be used, at the same time, as a unit of modularity, of isolation, of mobility, and of passivation. Specifically, Oz/K is a kernel programming language, that adds to the Oz computation model a notion of locality borrowed from the Kell calculus.

Conference and Workshop Papers

Type systems for the Dream framework

Building complex software architectures can be subject to subtle assemblage errors that are typically not captured by classical type systems available with host programming languages such as Java, C#, or ML. Our real-life motivating example is the Dream component-based framework, that has been developed to facilitate the construction of configurable communication subsystems. To avoid assemblage errors in the Dream framework, we introduce a new type system, together with its type checking and type inference algorithms. Our type system can actually be used with any model where components interact by exchanging structured messages on ports. Types in our system build approximations of component behaviors, and allow verifying that message handling operations remain consistent within a whole configuration. Technically, our type system combines extensible record types with row variables, together with set and process types. Inference is aided by the use of sparse type annotations, and operates by propagating type information in a configuration graph.

Conference and Workshop Papers