Thursday 19th–Friday 20th December, 2019
If you are starting from Glasgow on Thursday morning, we have a bus which will leave at 9.00am from the Hilton Glasgow Grosvenor Hotel. This is also the hotel in which most of the non-Glasgow people are staying on Wednesday night.
If you are arriving at Glasgow Airport on Thursday morning, take a taxi to Lodge on Loch Lomond.
If you are arriving in Glasgow by train on Wednesday evening, the hotel is close to Hillhead subway station. You can take the subway from St Enoch station, which is close to Glasgow Central station.
We will return to Glasgow by bus on Friday afternoon. If you are flying on Friday evening, you can take a taxi from Lodge on Loch Lomond directly to Glasgow airport.
If you have asked for accommodation in Glasgow on Wednesday night, then this is at the Hilton Glasgow Grosvenor Hotel.
We have a reservation at Cafe Andaluz West End, Cresswell Lane, at 7.30pm. This is very close to the Hilton Glasgow Grosvenor Hotel.
| 9:30-10:30 | Steve Ross-Talbot - TBC |
| 10:30-11:00 | Coffee break |
| 11:00-12:00 | Nobuko Yoshida, Simon Gay, Philip Wadler - ABCD: A Retrospective |
| 12:00-12:30 | Discussion of the achievements of ABCD |
| 12:30-13:30 | Lunch |
| 13:30-14:30 | Everyone - Lightning talks, 2 minutes each with 1 slide |
| 14:30-15:00 | Discussion about how to maintain the session types community in the future |
| 15:00-15:30 | Coffee break |
| 15:30 | Departure. The bus to Glasgow leaves at 15.30. |
Go is a popular concurrent programming language thanks to its ability to efficiently combine concurrency and systems programming. In Go programs, a number of concurrency bugs can be caused by a mixture of data races and communication problems. In this work, we develop a theory based on behavioural types to statically detect data races and deadlocks in Go programs. We first specify mutex safety/liveness and data race properties over a Go program model, using the happens-before relation defined in the Go memory model. We then represent these properties of programs in a μ-calculus model of types, and validate them using type-level model-checking. This is, to the best of our knowledge, the first static verification framework of this kind for the Go language, uniformly analysing concurrency errors caused by a mix of shared memory accesses and asynchronous message-passing communications.
We present a type-based analysis that ensures memory safety and object protocol completion in the language Mungo, a non-trivial subset of Java including generics. Objects are annotated with usages, typestates-like specifications of the admissible sequences of method calls. The analysis combines controlling the order in which methods are called by usage checking with a static check that determines if references con- tain null values. This interdependence yields a refined static analysis: type-safety not only ensures the absence of null pointer dereferencing and memory leaks, a safety property, but also that the intended usage protocol of each object is respected and completed, a liveness property. The type system is implemented in the form of a typechecker in Haskell.
In this talk I will discuss some issues that arise when defining a binary session type system for the higher order pi-calculus that also allows for dependent types. I will present a possible solution that avoids an explicit quantitative labelling.
[Ongoing work with Francisco Ferreira and Nobuko Yoshida]
Multiparty Session Types (MPST) are a type formalism used to model communication protocols among components in distributed systems, by specifying type and direction of data transmitted. It is standard for multiparty session type systems to use access control based on linear or affine types. While useful in offering strong guarantees of communication safety and session fidelity, linearity (resp. affinity) run into the well-known problem of inflexible programming, excluding scenarios that make use of shared channels or need to store channels into shared data structures.
In this paper, we develop capability-based access control for multiparty session types. In this setting, channels are split into two entities, the channel itself and the capability of using it. This gives rise to a more flexible session type system, which allows channel references to be shared and stored in persistent data structures. We prove that the resulting language retains session fidelity and illustrate it through a producer-consumer example.
[Joint work with Ornela Dardha and Simon Gay]
This work addresses a problem found in the construction of Service Oriented Architecture: the adaptation of service protocols with respect to functional redundancy and heterogeneity of global communication patterns. We intend to utilise the theory of Multiparty Session Types (MPST). Our approach is based upon a notion of a multiparty session type isomorphism that provides a constructive realisation of service adapter code when establishing equivalence. We achieve this by employing trace semantics over a collection of local types and introducing meta abstractions over the syntax of global types. We develop a corresponding equational theory for Multiparty Session type isomorphisms. The main motivation for this line of work is to define the type isomorphism that would allow to assess whether two components/services are substitutable modulo adaptation code, given component specification is considered to be a session type.
In the last year, we have mechanised the proof of subject reduction for binary session types. Along the way, we learned things about the presentation of type systems, alpha-equivalence in process types and developed a library that implements multiple name scopes, and a versatile representation for environments. In this talk we will summarise that, and present our ongoing effort to extend this work to multiparty session types and our plans to build upon the mechanisation to build a library of certified code for multiparty session types.
This talk presents a new static performance analysis framework for message-passing concurrent and distributed systems, based on the theory of multiparty session types (MPST). Understanding the run-time performance of concurrent and distributed systems is of great importance for the identification of bottlenecks and optimisation opportunities. In the message-passing setting, these bottlenecks are generally communication overheads and synchronisation times. Despite its importance, reasoning about these intensional properties of software, such as performance, has received little attention, compared to verifying extensional properties, such as correctness. Session Types, as behavioural protocol specifications, capture not only extensional, but also intensional properties of concurrent and distributed systems. Our approach augments MPST with communication latency and local computation cost information, that we use to extract cost equations from protocol descriptions. We apply our tool to different existing benchmarks in the literature of multiparty session types, implemented in C, MPI-C, Go and OCaml. We show that we can predict a tight upper-bound on the real execution costs.
The Elm programming language pioneers the Model-View-Update (MVU) architecture for writing web applications in a functional style. Although popular amongst developers, MVU has not been studied formally; it is therefore difficult to reason about any extensions, and each implementer must re-discover the essence of the architecture.
We introduce lambda-mvu, a formal description of the MVU architecture as a concurrent lambda-calculus, and prove its correctness. We modularly extend lambda-mvu with subscriptions and commands as found in the Elm programming language. We then further extend the calculus with linearity and model transitions, which are sufficient to allow us to provide the first formal integration of session-typed communication in a GUI framework. We implement our approach in the Links tierless web programming language, and show examples including a two-factor authentication workflow and multi-room chat server.
We present a toolchain for static verification of event-driven distributed programs. First, we implement a new verification methodology for multiparty protocols with data refinements. Our toolchain verifies protocols with recursive invariants on protocol states and utilises bounded model checking to ensure protocol correctness. Our tool is an extension of the protocol description language Scribble, and is formally founded on the theory of multiparty session types (MPST). We generate code of event style APIs in F*, a functional programming language aimed at program verification, from a refined Scribble protocol. Developers implement multiparty protocols as a set of callbacks and use the expressive type system of F* to validate their implementation against refinement types derived from the protocol. Our programming methodology does not require any runtime checks on protocol constraints and our toolchain is the first to achieve fully static verification of MPST-based protocols.
I will talk about Effpi: an experimental toolkit for strongly-typed concurrent and distributed programming in Dotty, a.k.a. Scala version 3.
Effpi addresses a main challenge in the development of concurrent programs: errors like protocol violations, deadlocks, and livelocks are often spotted late, at run-time, when applications are tested or (worse) deployed. Effpi aims at finding such errors early, when code is written and compiled.
Effpi provides: (1) a set of Dotty classes for describing communication protocols as types; (2) an embedded DSL for concurrent programming (reminiscent of Akka Typed); (3) a Dotty compiler plugin to verify whether p rotocols and programs enjoy desirable properties, such as deadlock-freedom; and (4) an efficient run-time system for executing Effpi's programs.
The combination of (1) and (2) allows the Dotty compiler to check whether an Effpi program implements a desired protocol/type; and this, together with (3), means that many concurrent programming errors are found and reported at compile-time. Further, (4) allows to run highly concurrent Effpi programs with millions of interacting processes/actors, by scheduling them on a limited number of CPU cores. In this talk, I will give an overview of Effpi, illustrate its design and main features, and discuss its future. I will also show how Effpi takes advantages of Dotty's new features.
One way to check communication protocols is by using session types. Protocols can be binary, one to one, or multiparty, many to many, each one with their own set of rules. Session types have already been implemented in various languages including Python and C. Differently than existing implementations of binary session types in Rust, ours supports multiparty protocols. As a concrete example, we created a server which interacts with various clients in Rust communicating through an MQTT broker with protocols that have been checked by our code.
The Go programming language was released by Google a decade ago, and recently its authors have considered how to extend it with generic types. This paper describes a design for generics in Go founded in the principles of programming languages, inspired by previous work on Featherweight Java by Igarashi, Pierce, and Wadler. We begin by presenting Featherweight Go (FG), a simplified version of the Go language, and Featherweight Generic Go (FGG), an extension of FG to support generic types. For each we show standard preservation and progress results. Finally, we show that FGG can be translated into FG by a process known as monomorphisation, and show that the translation preserves typing and operational semantics.
[Joint work with Robert Griesemer, Raymond Hu, Wen Kokke, Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida]
TBC
We will summarise and reflect on the progress and achievements of the whole project.