Speakers
Jesper Bengtson
IT University of Copenhagen, Denmark
Title: Asynchronous Session-Type Based Reasoning in Separation Logic
Abstract: Message passing is a useful abstraction for implementing concurrent programs. For real-world systems, however, it is often combined with other programming and concurrency paradigms, such as higher-order functions, mutable state, shared-memory concurrency, and locks. This talk details our recent work with the Actris logic, which we designed to reason about the functional correctness of concurrent programs that use a combination of these features. Actris combines the power of modern concurrent separation logics with a first-class protocol mechanism — based on session types — for reasoning about asynchronous message passing in the presence of other concurrency paradigms. Additionally, Actris supports a notion of sub protocols — based on session-type subtyping — that permits additional flexibility when composing channel endpoints. Finally, we demonstrate a semantic approach to binary asynchronous affine session types using logical relations. This approach allows us to not only type check programs using typing rules in the standard way, but also to manually prove typing judgements for racy, yet safe, programs that cannot be type checked using only the rules of the type system. All of our results have been mechanised using the Iris program logic in Coq.
Andreia Mordido
University of Lisbon, Portugal
Title: Beyond regular session types
Abstract: Traditional session types capture communication patterns characterized by regular languages. However, we know that many useful languages are not regular. In this talk, we will explore session types that live beyond the expressive power of regular languages. Seeking inspiration in deterministic pushdown automata, we will explore the patterns of interaction captured by context-free session types and nested session types. Throughout the talk, we will illustrate the new challenges that this gain in expressiveness brings to type equivalence and go through the key rules for designing a practical type equivalence algorithm.
MRG
David Castro-Perez (University of Kent, UK)
Francisco Ferreira-Ruiz (Imperial College, UK)
Lorenzo Gheri (Imperial College, UK)
Title: A Gentle Adventure Mechanising Message Passing Concurrency Systems
Abstract: We will discuss three aspects of mechanising binary and multiparty session types in the Coq proof assistant. We will talk about mechanising binary session types with a locally nameless binder representation (a deep embedding of binders), the design of Zooid a multiparty process language that favours shallow embeddings of binders. And finally, our mechanisation of trace equivalence for global, and local types, and with Zooid process traces. This will be presented as a tutorial designed from simplified versions of our mechanisation of binary and multiparty session types that are both more accessible and provide excercises.