Menu
Home
People
Publications
Collaborations
Research Topics
Control
Semantics
Synergy
System Support
Contact/Visit us
Intranet
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.
- Calculus and Language: design of the calculus itself, its syntax and semantics, its extension into a programming language, and extensions such as sharing and multistage and transparent kells.
- Formal Properties: creation of formal tools to guarantee some properties of Kell calculus terms, such as type systems and bisimulations. Use of these tools to study failures, transactions, and compensable actions in the calculus.
- Fractal Modelisation: instantiation of the Kell calculus in FraKtal, a calculus able to faithfully model the Fractal component model.
- Implementation: study of implementation strategies and realization of implementations of the Kell calculus.
Journal papers
- The Kell Calculus: A Family of Higher-Order Distributed Process Calculi. Alan Schmitt and Jean-Bernard Stefani. In LNCS volume of the post-proceedings of the Global Computing 2004 workshop, Venice, Italy, 2004. (34 pages)
This paper presents the Kell calculus, a family of distributed process calculi, parameterized by languages for input patterns, that is intended as a basis for studying component-based distributed programming. The Kell calculus is built around a pi-calculus core, and follows five design principles which are essential for a foundational model of distributed and mobile programming: hierarchical localities, local actions, higher-order communication, programmable membranes, and dynamic binding. The paper discusses these principles, and defines the syntax and operational semantics common to all calculi in the Kell calculus family. The paper provides a co-inductive characterization of contextual equivalence for Kell calculi, under sufficient conditions on pattern languages, by means of a form of higher-order bisimulation called strong context bisimulation. The paper also contains several examples that illustrate the expressive power of Kell calculi.
Conference and Workshop Papers
- Howe's method for calculi with passivation. Sergueï Lenglet, Alan Schmitt, and Jean-Bernard Stefani. In Proceedings of the 20th International Conference on Concurrency Theory (CONCUR 2009), Bologna, Italy, September 2009.
- Normal bisimulations in process calculi with passivation. Sergueï Lenglet, Alan Schmitt, and Jean-Bernard Stefani. In Luca de Alfaro, editor, Proceedings of the 12th International Conference on Foundations of Software Science and Computational Structures (FOSSACS 2009), volume 5504 of Lecture Notes in Computer Science, pages 257-271, York, United Kingdom, March 2009. Springer.
- On the Expressiveness and Decidability of Higher-Order Process Calculi. Ivan Lanese, Jorge A. Pérez, Davide Sangiorgi, and Alan Schmitt. In Proceedings of the 23rd Annual IEEE Symposium on Logic in Computer Science (LICS 2008), pages 145-155, June 2008.
- Component-Oriented Programming with Sharing: Containment is not Ownership. Daniel Hirschkoff, Tom Hirschowitz, Damien Pous, Alan Schmitt, and Jean-Bernard Stefani. In 4th International Conference on Generative Programming and Component Engineering (GPCE), Tallinn, Estonia, September 2005.
- An Abstract Machine for the Kell Calculus. Philippe Bidinger, Alan Schmitt, and Jean-Bernard Stefani. In 7th IFIP International Conference on Formal Methods for Object-Based Distributed Systems (FMOODS), Athens, Greece, June, 2005. This paper obtained the Best Paper Award.
- The Kell calculus: operational semantics and type system. Philippe Bidinger and Jean-Bernard Stefani. In Proceedings 6th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems(FMOODS 2003), Paris, France, November 19-21, 2003. (c) Springer-Verlag.
- The M-calculus: A Higher-Order Distributed Process Calculus. Alan Schmitt and Jean-Bernard Stefani. In Proceedings of the 30th Annual ACM Symposium on Principles of Programming Languages (POPL), New Orleans, LA, USA, January 17-19, 2003. (c) ACM.
- A Calculus of Kells. Jean-Bernard Stefani. In Proceedings of the 2nd International Workshop on Foundations of Global Computing, Eindhoven, the Netherlands, June 28-29, 2003.
Technical Reports
- A Calculus of Higher-Order Distributed Components. Jean-Bernard Stefani. RR-4692. SARDES project, January 2003.
- The M-calculus: a Higher-Order Distributed Process Calculus. Alan Schmitt and Jean-Bernard Stefani. RR-4361. SARDES project, January 2002.
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
- Oz/K: A Kernel Language for Component-Based Open Programming. Michaël Lienhardt, Jean-Bernard Stefani, and Alan Schmitt. In ACM, editor, 6th International Conference on Generative Programming and Component Engineering (GPCE'07), pages 43-52, October 2007.
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
- Typing Component-Based Communication Systems. Michaël Lienhardt, Claudio Antares Mezzina, Alan Schmitt, and Jean-Bernard Stefani. In Proceedings of the 11th Formal Methods for Open Object-Based Distributed Systems (FMOODS) & 29th Formal Techniques for Networked and Distributed Systems (FORTE), June 2009.
- Typing Communicating Component Assemblages. Michaël Lienhardt, Alan Schmitt, and Jean-Bernard Stefani. In Proceedings of the 7th International Conference on Generative Programming and Component Engineering (GPCE'08), pages 125-136, Nashville, TN, USA, October 2008.
- Dream Types - A Domain Specific Type System for Component-Based Message-Oriented Middleware. Philippe Bidinger, Matthieu Leclercq, Vivien Quéma, Alan Schmitt and Jean-Bernard Stefani. In Proceedings of the 4th Workshop on Specification and Verification of Component-Based Systems (SAVCBS'05), in association with ESEC/FSE'05, Lisbon, Portugal, September 2005.
Presentations
- DreamTypes: Systèmes de Types pour Dream, ICAR 2006 (français)