https://www.dagstuhl.de/21372

12. – 17. September 2021, Dagstuhl-Seminar 21372

Behavioural Types: Bridging Theory and Practice

Organisatoren

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)

Auskunft zu diesem Dagstuhl-Seminar erteilen

Jutka Gasiorowski zu administrativen Fragen

Michael Gerke zu wissenschaftlichen Fragen

Dagstuhl Reports

Wir bitten die Teilnehmer uns bei der notwendigen Dokumentation zu unterstützen und Abstracts zu ihrem Vortrag, Ergebnisse aus Arbeitsgruppen, etc. zur Veröffentlichung in unserer Serie Dagstuhl Reports einzureichen über unser
Dagstuhl Reports Submission System.

Dokumente

Teilnehmerliste
Gemeinsame Dokumente
Dagstuhl-Seminar Wiki
Programm des Dagstuhl-Seminars [pdf]

(Zum Einloggen bitte persönliche DOOR-Zugangsdaten verwenden)

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

Dokumentation

In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.

 

Download Übersichtsflyer (PDF).

Publikationen

Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von
Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.