Document Open Access Logo

Behavioural Types: Bridging Theory and Practice (Dagstuhl Seminar 21372)

Authors Mariangiola Dezani, Roland Kuhn, Sam Lindley, Alceste Scalas and all authors of the abstracts in this report



PDF
Thumbnail PDF

File

DagRep.11.8.52.pdf
  • Filesize: 4.06 MB
  • 24 pages

Document Identifiers

Author Details

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
and all authors of the abstracts in this report

Cite AsGet BibTex

Mariangiola Dezani, Roland Kuhn, Sam Lindley, and Alceste Scalas. Behavioural Types: Bridging Theory and Practice (Dagstuhl Seminar 21372). In Dagstuhl Reports, Volume 11, Issue 8, pp. 52-75, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/DagRep.11.8.52

Abstract

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). An earlier Dagstuhl Seminar, 17051 "Theory and Applications of Behavioural Types" (January 29-February 3, 2017), played an important role in coordinating this effort. 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). In this seminar, experts from academia and industry explored together how best to bridge the gap between theory and mainstream practice. They tackled challenges that are fundamental in practical systems development, but are rarely or only partially addressed in the behavioural types literature - in particular, failure handling, asynchronous communication, and dynamic reconfiguration. Moreover they explored how the tools of behavioural types and programming languages theory (such as linearity, gradual types, and dependent types) can help to address these challenges.

Subject Classification

ACM Subject Classification
  • Theory of computation → Models of computation
  • Theory of computation → Process calculi
  • Theory of computation → Type structures
Keywords
  • behavioural types
  • concurrency
  • programming languages
  • session types

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail