December 2017 Meeting


18–19 December, 2017


Room G.07, Informatics Forum, The University of Edinburgh


The Informatics forum is in easy walking distance of central Edinburgh and Edinburgh Waverley train station. If arriving at Edinburgh airport, either the AirLink bus service or Edinburgh trams can be taken to central Edinburgh.

Tentative Schedule

Monday 18th December

13:30-14:00Philip Wadler (Edinburgh) -- Gradual session types
14:00-14:30Dimitris Kouzapas (Cyprus) and Laura Voinea (Glasgow) -- A session type system for asynchronous unreliable broadcast communication
14:30-15:00Simon Fowler (Edinburgh) -- Session types without tiers
15:00-15:30Coffee break
15:30-16:00Laura Bocchi (Kent) -- From time-sensitive models to time-sensitive programs
16:00-16:30Alceste Scalas (Imperial) -- Multiparty session types, beyond duality
16:30-17:00Coffee break
17:00-17:30Ornela Dardha (Glasgow) -- A new linear logic for deadlock-free session-typed processes
17:30-18:00Wen Kokke (Edinburgh) -- Taking apart classical processes
19:00-Dinner, Roti

Tuesday 19th December

09:00-09:30Frank Pfenning (Carnegie Mellon) -- Adjoint logic and its concurrent semantics
09:30-10:00Vasco Vasconcelos (Lisbon) -- Specifying and testing REST application interfaces
10:00-10:30Coffee break
10:30-11:00Rumyana Neykova (Imperial) -- Let it recover: multiparty protocol-induced recovery
11:00-11:30Steve Ross-Talbot (Estafet) -- Why microservices fail and how Scribble can by used to mitigate those failures
11:30-12:00Coffee break
12:00-12:30Gary Brown (Red Hat) -- Scribble in an agile cloud native world
12:30-13:00Raymond Hu (Imperial) -- Some demos of recent and ongoing work on the Scribble tools
14:00-14:30Status reports
14:30-16:00Advisory board meeting

Progress Report

A progress report detailing the ABCD team's progress against the original work packages in 2017 can be found here.

Talk Abstracts

Laura Bocchi: From time-sensitive models to time-sensitive programs

I will present recent and ongoing work, based on automata and session types, towards supporting the verification of real-world time-sensitive programs. The talk will centre on a theory of refinements for timed asynchronous systems, in the formal setting of Communicating Timed Automata. I will introduce three notions of (compositional and decidable) refinement, serving as a formal counter-part of concrete implementations with time-sensitive programming primitives. I will then establish conditions under which the given refinements preserve the behaviour of systems and their progress properties. All our results build upon new semantics of CTAs, that are needed to faithfully model the behaviour of real-time primitives of mainstream programming languages.

Gary Brown: Scribble in an agile cloud native world

This talk (and demo) will review how technology has changed through the life of the ABCD project and will discuss how Scribble could be used in the future.

Ornela Dardha: A new linear logic for deadlock-free session-typed processes

The π-calculus, viewed as a core concurrent programming language, has been used as the target of much research on type systems for concurrency. We propose a new type system for deadlock-free session- typed π-calculus processes, by integrating two separate lines of work. The first is the propositions-as-types approach by Caires and Pfenning, which provides a linear logic foundation for session types and guarantees deadlock-freedom by forbidding cyclic process connections. The second is Kobayashi's approach in which types are annotated with priorities so that the type system can check whether or not processes contain genuine cyclic dependencies between communication operations. We combine these two techniques for the first time, and define a new and more expressive variant of classical linear logic with a proof assignment that gives a session type system with Kobayashi-style priorities. This can be seen in three ways: (i) as a new linear logic in which cyclic structures can be derived and a cycle-elimination theorem generalises cut-elimination; (ii) as a logically- based session type system, which is more expressive than Caires and Pfenning's; (iii) as a logical foundation for Kobayashi's system, bringing it into the sphere of the propositions-as-types paradigm.

Simon Fowler: Session types without tiers

Session types statically guarantee that concurrent communication complies with a protocol. However, most accounts of session typing do not handle failure, which means they are of limited use in distributed settings where failure is pervasive.

We give the first formal account of session typing with failure handling in a functional programming language. We define a core calculus which satisfies preservation and progress properties, is deadlock free, data-race free, and terminating.

We provide the first implementation of session typing with failure handling for a fully fledged functional programming language, by extending the Links web programming language. Our implementation draws on existing work on algebraic effects and effect handlers. We illustrate our implementation through a chat server application for the web, in which all communication occurs over session typed channels and disconnections are handled gracefully.

(Joint work with Sam Lindley, J. Garrett Morris, and Sara Decova)

Raymond Hu: Some demos of recent and ongoing work on the Scribble tools

We will demonstrate some of the recent and ongoing implementation work on the MPST-based Scribble tools: explicit connection actions, for protocols with dynamic/optional participants; index-parameterised roles, for dynamic instantiation of participants; and session type providers in F\#. Feedback on these ongoing works is very welcome.

Dimitrios Kouzapas and Laura Voinea: A session type system for asynchronous unreliable broadcast communication

Communication patterns arising in concurrent programming can benefit from being formally specified. Session types are such formal specifications, that guarantee desired communication behaviour. However, up to now, session type systems have assumed that communication is reliable, without message loss. This excludes a wide class of distributed systems, where unreliable communication is common, such as ad-hoc networks or wireless sensor networks. To address this, we introduce a process calculus with unreliable broadcast communication, equipped with a sound session type system. Broadcast and gather operations, common in such networks, are captured by our asynchronous semantics, in the presence of message loss. Message loss may lead to unsynchronised session endpoints. To further account for unreliability we propose a recovery mechanism that corresponds to real time conditions. Our type system ensures safety between all synchronised endpoints within a session. We show that dropping session endpoints, when internal conditions are met, is safe. We demonstrate the expressiveness of our framework by implementing Paxos, the textbook protocol for reaching consensus in an unreliable, asynchronous network.

Frank Pfenning: Adjoint logic and its concurrent semantics

We present adjoint logic as a framework to combine multiple logics with varying structural properties through adjoint modal operators. We then endow its sequent calculus with process expressions and a uniform operational semantics, which specializes to asynchronous session-typed communication for modes that do not allow contraction. On modes with contraction we obtain multicast communication, copy-on-receive, and distributed garbage collection, all of which arise in a natural way from the logical foundations.

[joint work with Klaas Pruiksma and William Chargin]

Rumyana Neykova: Let it recover: multiparty protocol-induced recovery

Fault-tolerant communication systems rely on recovery strategies which are often error-prone (e.g. a programmer manually specifies recovery strategies) or inefficient (e.g. the whole system is restarted from the beginning). In this talk, we will present an algorithm to efficiently compute a safe global state from which a system of interacting processes should be recovered. We statically analyse the communication flow of a program, given as a multiparty protocol, to extract the causal dependencies between processes and to localise failures. We formalise our recovery algorithm and prove its safety. A recovered communication system is free from deadlocks, orphan messages, and reception errors. Our recovery algorithm incurs less communication cost (only affected processes are notified) and overall execution time (only required states are repeated). On top of our analysis, we design and implement a runtime framework in Erlang where failed processes and their dependencies are soundly restarted from a computed safe state. We evaluate our recovery framework on message-passing benchmarks and a use case for crawling web pages. The experimental results indicate our framework outperforms a built-in static recovery strategy in Erlang when a part of the protocol can be safely recovered.

Alceste Scalas: Multiparty session types, beyond duality

Multiparty Session Types (MPST) are a typing discipline for message-passing programs: given a session protocol S involving two or more parties, MPST checking ensures that a program implements S without errors.

In this talk, I'll demonstrate that the MPST subject reduction property is surprisingly restrictive: there are very simple protocols for which no implementation can be proven type-safe. I will show that such restrictions are subtly related to binary duality; then, I will present a revised MPST theory that removes such limitations.

Vasco Vasconcelos: Specifying and testing REST application interfaces

REST APIs are nowadays a popular tool to program web services. The correct development of server and client code requires well documented interfaces. Despite initiatives such as the Open API Specification, the support for the description of such interfaces is currently quite limited, focusing essentially on syntactic aspects. We present HeadREST, a language intended to describe the semantic aspects of REST APIs. We show a testing technique aiming at verifying the compliance of a REST API against its HeadREST spec. [Joint work with Fábio Ferreira, Telmo Santos, Francisco Martins, and Antónia Lopes]

Philip Wadler: Gradual Session Types

Session types are a rich type discipline, based on linear types, that lift the sort of safety claims that come with type systems to communications. However, web-based applications and micro services are often written in a mix of languages, with type disciplines in a spectrum between static and dynamic typing. Gradual session types address this mixed setting by providing a framework which grants seamless transition between statically typed handling of sessions and any required degree of dynamic typing. We propose GradualGV as an extension of the functional session type system GV with dynamic types and casts. We demonstrate type and communication safety as well as blame safety, thus extending previous results to functional languages with session-based communication. The interplay of linearity and dynamic types requires a novel approach to specifying the dynamics of the language.