Preface

This volume contains the proceedings of PLACES 2024, the 15th edition of the Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software. The workshop is scheduled to take place in Luxembourg City, Luxembourg on April 6, 2024, as a satellite event of ETAPS, the European Joint Conferences on Theory and Practice of Software.

PLACES offers a forum for exchanging new ideas on how to address the challenges of concurrent and distributed programming, and how to improve the foundations of modern and future computer applications. PLACES welcomes researchers from various fields, and its topics include the design of new programming languages, models for concurrent and distributed systems, type systems, program verification, and applications in various areas (e.g. microservices, sensor networks, blockchains, event processing, business process management).

The Programme Committee of PLACES 2024 consisted of:

• Laura Bocchi, University of Kent, UK
• Cinzia Di Giusto, Université Côte d'Azur, CNRS, FR
• Juliana Franco, DeepMind, UK
• Lorenzo Gheri, University of Liverpool, UK
• Ping Hou, University of Oxford, UK
• Cosimo Laneve, University of Bologna, IT
• Matthew Alan Le Brun, University of Glasgow, UK
• Rumyana Neykova, Brunel University, UK
• Kirstin Peters, Universität Augsburg, DE
• Diogo Poças, LASIGE, Universidade de Lisboa, PT
• Shoji Yuen, Nagoya University, JP

After a thorough reviewing process, the Programme Committee has accepted five research papers (out of six original submissions): such papers are published in this volume. The Programme Committee has also accepted three talk proposals on preliminary or already-published work: the titles and abstracts of such talks are also listed in this volume. Each submission (research paper or talk proposal) was reviewed and discussed by three Programme Committee members on the EasyChair platform.

3 April 2024
Diana Costa and Raymond Hu

Simple MultiParty Sessions

Mariangiola Dezani-Ciancaglini (Università di Torino, IT)

Simple MultiParty Sessions (SMPS) do not have channels, session initiators and the distinction between compile time and run time syntax. They are based only on participant names and input/output processes. They are equipped with global types without requiring projections and local types. In this presentation we will discuss pros and cons of SMPS. On the good side SMPS allow to easily describe internal delegation, partial typing and session composition. On the bad side SMPS are less expressive than standard MultiParty Sessions. In particular interleaved sessions with crossing delegations cannot be represented.

Verified Secure Routing

Peter Müller (ETH Zurich, CH)

SCION is a new Internet architecture that addresses many of the security vulnerabilities of today's Internet. Its clean-slate design provides, among other properties, route control, failure isolation, and multi-path communication. The verifiedSCION project is an effort to formally verify the correctness and security of SCION. It aims to provide strong guarantees for the entire architecture, from the protocol design to its concrete implementation. The project uses stepwise refinement to prove that the protocol withstands increasingly strong attackers. The refinement proofs assume that all network components such as routers satisfy their specifications. This property is then verified separately using deductive program verification in separation logic. This talk will give an overview of the verifiedSCION project and explain, in particular, how we verify code-level properties such as memory safety, I/O behavior, and information flow security.

Presentations of Preliminary or Already-Published Work

PLACES 2024 welcomed the submissions of talk proposals (describing preliminary or already-published work) that could spark interesting discussion during the workshop. This is the list of all accepted talk proposals.

Multiparty Session Type Projection and Subtyping with Automata

Elaine Li - New York University, USA
Felix Stutz - MPI-SWS, DE
Thomas Wies - New York University, USA

Multiparty session types (MSTs) are a type-based approach to verifying communication protocols. Central to MSTs is a projection operator: a partial function that maps protocols represented as global types to correct-by-construction implementations for each participant, represented as a communicating state machine (CSM). Existing projection operators are syntactic in nature, and trade efficiency for completeness. In the first part of the talk, I will present the first projection operator that is sound and complete. I will highlight the automata-theoretic nature of our projection operator, which separates synthesis from checking implementability, and can be computed in PSPACE.

While our projection operator always computes a candidate implementation if one exists, it may not always compute the best candidate. In the second part of the talk, I motivate three variations of the subtyping problem for MSTs. I highlight differences between the problems in terms of complexity, compositionality and context-dependence. I show how our previous solution to implementability gives rise to solutions to subtyping problems for MSTs, with unrestricted CSMs as implementation model.

Hapi - Implementing the asynchronous π-calculus with multiparty session types

Lasse Nielsen - Denmark
Nobuko Yoshida - University of Oxford, UK

We introduce the language hapi, implementing the asynchronous π-calculus with multiparty session types. Hapi offers type verification and compilation of the calculus into C++. The direct syntax representation of the π-calculus with multiparty session types in hapi enables a concise declaration of message-passing processes. Hapi's type verification guarantees a linear usage of channels, type safety, no race-conditions and progress properties of hapi processes.

Multiparty Session Type Inference for a Rust DSL

Walid Nawfal Sabihi, Martin Vassor and Nobuko Yoshida - University of Oxford, UK

Multiparty Session Types (MPSTs) have traditionally been used in a top-down manner, starting from a global type which provides a specification for the system, that is then projected onto local types that are used to type-check each participant in the protocol. This approach is challenging to adopt for existing systems that need to gradually integrate MPSTs but have not yet defined a global type that fully covers their behaviour.
In this talk, we propose an inference system for a subset of Rust programs, synthesising anonymous local session types. We also discuss a participant allocation algorithm that generates a global session type from a set of anonymous local session types, with guarantees for correctness and completeness.