Session Types in Concurrent Calculi: Higher-Order Processes and Objects

Abstract

This dissertation investigates different formalisms, in the form of programming language calculi, that are aimed at providing a theoretical foundation for structured concurrent programming based on session types. The structure of a session type is essentially a process-algebraic style description of the behaviour of a single program identifier serving as a communication medium (and usually referred to as a channel): the types incorporate typed inputs, outputs, and choices which can be composed to form larger protocol descriptions. The effectiveness of session typing can be attributed to the linear treatment of channels and session types, and to the use of tractable methods such as syntactic duality to decide if the types of two connected channels are compatible. Linearity is ensured when accumulating the uses of a channel into a composite type that describes also the order of those actions. Duality provides a tractable and intuitive method for deciding when two connected channels can interact and exchange values in a statically determined type-safe way. We present our contributions to the theory of sessions, distilled into two families of programming calculi, the first based on higher-order processes and the second based on objects. Our work unifies, improves and extends, in manifold ways, the session primitives and typing systems for the Lambda-calculus, the Pi-calculus, the Object-calculus, and their combinations in multi-paradigm languages. Of particular interest are: the treatment of infinite interactions expressed with recursive sessions; the capacity to encapsulate channels in higher-order structures which can be exchanged and kept suspended, i.e., the use of code as data; the integration of protocol structure directly into the description of objects, providing a powerful and uniformly extensible set of implementation abstractions; finally, the introduction of asynchronous subtyping, which enables controlled reordering of actions on either side of a session. Our work on higher-order processes and on object calculi for session-based concurrent programming provides a theoretical foundation for programming language design integrating functional, process, and object-oriented features.