Communication-based Computation: Practicalities of Programming with Sessions
8-9 June, 2015. School of Computing Science, University of Glasgow
Theoretical work on session types and other forms of behavioural typing continues apace. Yet these ideas have gained little traction in practical languages outside the research community. What can we learn from the research languages that exist today?
At this two-day meeting, we plan to focus on the practicalities of programming with session types: strengths and weaknesses of existing approaches, potential obstacles to adoption, and integration with existing programming paradigms, such as functional and object-oriented programming. Tool and compiler demonstrations are of particular interest, but workshop-style talks on related issues are also welcome.
Demo and talk proposals on any topic that fits within the overall focus are encouraged. The following are some things that we find interesting, but feel free to surprise us. Theoretical content is welcomed as long as its relevance to programming practice is made clear.
We will have long slots (45 minutes) to allow for discussion time and audience interaction. The speaker should expect to present 20-25 minutes worth of material, with discussion taking place during the presentation as well as at the end. If we finish before the 45 minutes are up, we will take a short break before the next speaker. We will ask laptops to be put away during the talks to encourage as much participation as possible.
Monday, 8 June
|9:30 – 9:45||Welcome|
|9:45 – 10:30||Raymond Hu||
Generating endpoint APIs from multiparty session types
We will demonstrate a work-in-progress tool for generating Java endpoint APIs from multiparty session types written in Scribble. The aim is to automatically produce APIs similar to those used in current practices, to minimise restrictions on endpoint implementation or integration with other development facilities, while promoting session type safety via the native type system of the target language. As much of the static session typing constraints for the source protocol is captured in the native Java API as possible, with the remainder of the session safety aspects handled by lightweight run-time checks built into the generated API.
|10:30 – 11:15||Luca Padovani||
Linearity and the Pi Calculus, Revisited
We discuss a type system that extends the linear pi calculus with pairs, disjoint sums, and regular data types. The type system adopts a different approach to linearity: on the one hand, it allows parallel processes to simultaneously access a data structure containing linear values; on the other hand, it provides stronger guarantees on the fact that linear channels are actually used. We demonstrate the type system at work on a series of examples and present a tool that implements the corresponding type reconstruction algorithm.
|11:15 – 11:45||Coffee break|
|11:45 – 12:30||J. Garrett Morris||
Lightweight Session Types in Links
Links is a functional programming language for n-tier application development. This talk will demonstrate some recent work on adding session-typed concurrency to Links, and the corresponding changes to Links type system. I will describe our approach to integrating linear types with an existing functional type system, based on the subkind mechanisms of Mazurak et al (2012). I will also talk about Links' mechanism for extensible records and variants, based on row typing, and how a similar approach can be applied to session types to capture many of the traditional uses of subtyping in type system based on parametric polymorphism.
|12:30 – 14:00||Lunch|
|14:00 – 14:45||Conor McBride||
Traffic-Dependent Session Types
Sending and receiving in session types resonate with the dependently typed notions of Sigma and Pi types, respectively. However, when we try to build a higher-order notion of session type from Sigma and Pi, we find we must take care upon what exactly dependent session types can depend. What gets substituted for the bound variables when we instantiate the range of such a type? I argue that the correct answer to this question is not the session *participant*, but the session *traffic*. I show how to construct in Agda a universe of session types which enforce dependency only on traffic, and I offer some interpretations of these types as sets of participating processes.
|14:45 – 15:30||Dennis Griffith||
Introduction to Sill
This talk will provide an overview of the language SILL, a session typed language currently under development at UIUC and CMU. SILL provides monadic process expressions, branching subtyping, both affine and linear types, and an integration of both synchronous and asynchronous communication. After an overview of the language, we will work through some examples demonstrating how these features play out in practice.
|15:30 – 16:00||Coffee break|
|16:00 – 16:45||Philip Wadler||
Propositions as Sessions: An Open Question
Simple types for lambda calculus guarantee that all programs terminate. Often this is just the property we want, but it rules out important cases such as general recursion. Fortunately, there is a workaround, in that the fixpoint combinator allows us to implement general recursion in a simply-typed setting. Session types for process calculus guarantee that all processes terminate and there are no races. Often this is just the property we want, but it rules out important cases such as a ticket system in which users may race to purchase the last ticket. What is the corresponding workaround?
Tuesday, 9 June
|9:45 – 10:30||Nicholas Ng||
Protocols by Default: Safe MPI Code Generation based on Session Types
In this talk I will present a code generation framework for type-safe and deadlock-free Message Passing Interface (MPI) programs. The code generation process starts with the definition of a global topology using Pabble, a protocol specification language based on parameterised multiparty session types (MPST). An MPI parallel program backbone is automatically generated from the global specification. The backbone code can then be merged with the sequential code describing the application behaviour, resulting in a complete MPI program. This merging process is fully automated through the use of an aspect-oriented compilation approach. In this way, programmers only need to supply the intended communication protocol and provide sequential code to automatically obtain parallelised programs that are guaranteed free from communication mismatch, type errors or deadlocks.
|10:30 – 11:15||Massimo Bartoletti||
A Contract-Oriented Middleware
Developing distributed applications typically requires to integrate new code with preexisting third-party services, e.g., e-commerce facilities, maps, etc. These services cannot always be assumed to smoothly collaborate with each other; rather, they live in a "wild" environment where they must compete for resources, and possibly diverge from the intended behaviour in case they find it convenient to do so.
To overcome this issue, some recent works have proposed to discipline the interaction of mutually distrusting services through behavioural contracts. The idea is a bottom-up composition, where only those services with compliant contracts can establish sessions through which they interact. We exploit a theory of timed behavioural contracts to design and implement a message-oriented middleware where distributed services can be dynamically composed, and their communications monitored so to guarantee safe interactions.
|11:15 – 11:45||Coffee break|
|11:45 – 12:30||Simon Fowler||
Monitoring Distributed Erlang/OTP Applications with Multiparty Session Types
Just as data types encode the data used in applications, session types encode communication patterns, providing guarantees that protocols are safe and that programs conform to their prescribed protocols. Traditionally, session types have been checked statically at compile time.
An alternative approach is to use session types as a tool for lightweight runtime verification. This is especially useful in languages with dynamically-checked types, and in languages where session participants cannot always be assumed to be available.
In this talk, I'll explain my work on adding dynamic monitoring of session types to distributed Erlang/OTP server applications. Building on the work on Multiparty Session Actors by Neykova and Yoshida, I'll talk about how session types fit into standard OTP design patterns such as supervision trees, how to detect and handle failures, and demonstrate some larger case studies such as a DNS server.
|12:30 – 14:00||Lunch|
|14:00 – 14:45||Dimitris Kouzapas||
Typechecking Protocols with Scribble and Mungo
This talk will demonstrate the current status of Mungo. Mungo is a tool developed to statically check/enforce typestate on Java objects. Based on a small subset of Java 1.4 without inheritance, Mungo can statically track the linear usage of fields, variables and parameters of a Java program according to a predeclared typestate. Our demonstration examples include the connection between statically enforced typestate and session types by using the Scribble tool to write session protocols and translate them into Mungo protocols.
|14:45 – 15:30||Edwin Brady||
Type-driven Development for Games and Protocols
Idris is a general purpose pure functional programming language with dependent types. In Idris, types are a first class language construct, meaning that they can be manipulated and computed like any other language construct. It encourages a type-driven style of development, in which programmers give types first and use interactive editing tools to derive programs. Introductory examples typically involve length preserving operations on lists, or ordering invariants on sorting.
Realistically, though, programming is not so simple: programs interact with users, communicate over networks, manipulate state, deal with erroneous input, and so on. In this talk I will show how advanced type systems allow us to express such interactions precisely, and how they support verification of stateful systems as a result.
The talk will include several examples, leading to a verified implementation of a word game (Hangman). I will show how Type-driven Development allows programmers to specify the game rules in a direct and concise style, and how it leads to an implementation, guaranteed to correctly follow the rules by type checking.
|15:30 – 16:00||Coffee break|
|16:00 – 16:45||Discussion|
The meeting will take place in the Sir Alwyn Williams building, where the School of Computing Science is located (room 423 on the Monday, and 422 on the Tuesday).
If you go this booking.com page and zoom in, you will find the university located between Hillhead, Kelvinbridge and Kelvinall subway stations. The Great Western Road is just to the north of the university and has a number of reasonably-priced hotels, all within a 10-minute walk of the school.
About 15 minutes away to the south east is Sauchiehall St. That also has several hotels and could be a more pleasant walk in the morning.
CoCo:PoPS is organised by Garrett Morris, Dimitris Kouzapas and Roly Perera. If you are interested in attending or presenting, please email Roly (firstname.lastname@example.org).