https://www.dagstuhl.de/21372

September 12 – 17 , 2021, Dagstuhl Seminar 21372

Behavioural Types: Bridging Theory and Practice

Organizers

Mariangiola Dezani (University of Turin, IT)
Roland Kuhn (Actyx AG – München, DE)
Sam Lindley (University of Edinburgh, GB)
Alceste Scalas (Technical University of Denmark – Lyngby, DK)

For support, please contact

Jutka Gasiorowski for administrative matters

Michael Gerke for scientific matters

Motivation

Behavioural types specify the way in which software components interact with one another. Unlike data types (which describe the structure of data), behavioural types describe communication protocols, and their verification ensures that programs do not violate such protocols. The behavioural types research community has developed a flourishing literature on communication-centric programming, exploring many directions. One of the most studied behavioural type systems are session types, introduced by Honda et al. in the ‘90s, and awarded with prizes for their influence in the past 20 and 10 years (by the ESOP and POPL conferences, respectively). Other varieties of behavioural types include typestate systems, choreographies, and behavioural contracts; research on verification techniques covers the spectrum from fully static verification at compile-time to fully dynamic verification at run-time.

In the last decade, research on behavioural types has shifted emphasis towards practical applications, using both novel and existing programming languages (e.g., Java, Python, Go, C, Haskell, OCaml, Erlang, Scala, Rust). Yet, despite the vibrant community and the stream of new results, the use of behavioural types for mainstream software development and verification remains limited.

This limitation is largely down to the rapid pace at which mainstream industrial practice for the design and development of concurrent and distributed systems evolves, often resulting in substantial divergence from academic research. In the absence of established tools to express communication protocols, widely used implementations concentrate solely on scalability and reliability. The flip side is that these systems are either overly loose, supporting any conceivable communication structure (via brokers), or overly restricted, supporting only simple request-response protocols (like HTTP or RPC).

This Dagstuhl Seminar brings together academic and industry experts who work in the areas of concurrency, distributed systems, and behavioural types. The goal is to explore how best to bridge the gap between behavioural types theory and mainstream software development practice: we believe that theory and practice must progress hand-in-hand, each taking cues from the other and pushing forward the state of the art.

During the seminar we hope to make tangible progress on at least the following key topics:

  • Failure handling: how to describe and handle errors and unexpected behaviours of distributed system components
  • Asynchronous communication: how to ensure the correct handling of issues like packet loss and time constraints
  • Dynamic reconfiguration: how to correctly design and implement applications with dynamic communication topology, e.g., based on the ubiquitous pub/sub model.

Motivation text license
  Creative Commons BY 3.0 DE
  Mariangiola Dezani, Roland Kuhn, Sam Lindley, and Alceste Scalas

Related Dagstuhl Seminar

Classification

  • Logic In Computer Science
  • Programming Languages
  • Software Engineering

Keywords

  • Concurrency
  • Behavioural types
  • Session types
  • Programming languages

Documentation

In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.

 

Download overview leaflet (PDF).

Publications

Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.