Dagstuhl-Seminar 21372
Behavioural Types: Bridging Theory and Practice
( 12. Sep – 17. Sep, 2021 )
Permalink
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)
Kontakt
- Michael Gerke (für wissenschaftliche Fragen)
- Jutka Gasiorowski (für administrative Fragen)
Dagstuhl Seminar Wiki
- Dagstuhl Seminar Wiki (Use personal credentials as created in DOOR to log in)
Programm
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.
This seminar followed the earlier Dagstuhl Seminar 17051 "Theory and Applications of Behavioural Types". Whereas Seminar 17051 was quite broad, encompassing both theory and practice across a wide range of areas relating to behavioural types, this seminar was much more focused, concentrating on how best to enable the use of behavioural types for practical programming.
Initial preparations
We gathered initial lists of proposed talks and breakout topics prior to the start of the seminar via an online form. We added to these throughout the week. We scheduled talks and breakout groups daily depending on audience interest and participant availability. The first part of the week was primarily talks, with ample time for stimulating discussions; the second part included more time for breakout sessions.
Hybrid seminar logistics
Due to the SARS-CoV-2 pandemic, the seminar was organised in hybrid format, with both in-person and remote participants. As the virtual participants came from a wide range of time zones (from central US to Japan) we gave special consideration to the time slot 2pm-4pm CEST during which everyone could attend. Those in Europe and Japan were able to attend morning sessions and those in Europe and America to attend further afternoon sessions (and a special evening session on Monday).
In order to run a successful hybrid Dagstuhl seminar, we made essential use of the dedicated equipment available at Dagstuhl: a Zoom-based streaming setup, with multiple cameras and ceiling microphones in the seminar room. All talks were live-streamed to both virtual and in-person participants. Talks were recorded so that virtual participants from incompatible time zones could catch up, then deleted at the end of the week. Larger hybrid breakout sessions were held in the main seminar room, and smaller ones elsewhere using a more ad hoc setup.
Moreover, all participants (local and virtual) were invited to use Zulip (a chat application) to exchange messages and files, pose questions during presentations, and remain informed on the upcoming events, group activities, and schedule updates.
Activities and outcomes
Throughout the seminar, the participants gathered in focused breakout groups: the findings of the breakout groups are described in more detail elsewhere in the report. Here is a brief summary:
- Typing non-channel-based models allowed researchers with a wide range of perspectives and backgrounds to exchange their views. A key observation was that modern concurrent systems that coordinate via streams of events are difficult to analyse and verify with using existing approaches, and new formalisms are needed.
- Logic-based approaches reviewed the state of the art, and discussed new directions. One of the conclusions is that more research is needed to relate concurrent and distributed systems to a broader range of logics beyond classical and intuitionistic linear logic (which are the focus of most current publications).
- Type-informed recovery strategies explored failure handling at different levels (from network to application), and summarised several open questions not addressed in existing work.
- Session types with untrusted counter-parties focused on how to ensure that different processes interact under compatible protocols, establishing the beginning of new work on monitoring and adaptation.
- Join patterns / synchronisation - the next generation collected a survey of various attempts to integrate join patterns in programming languages, and discussed why they have not yet become mainstream. The discussion highlighted the need for exploring the connections between join patterns and linear logic, and the use of the join calculus as a reference for new implementation attempts.
The participants of several breakout groups have agreed to continue their work and collaboration after the seminar.
In addition to these more structured breakout sessions there were further lively improvised meetings and discussions (especially after dinner) which are not summarised in the report.
Overall, we believe that the seminar activities were a success. Unfortunately the hybrid format did pose a barrier for remote participants, especially those in different time zones. But on the positive side, for many participants this was their first Dagstuhl seminar, and for the in-person participants it was their first in-person scientific gathering after many months of virtual events due to the SARS-CoV-2 pandemic: their feedback has been enthusiastic.
At the end of the seminar the participants agreed to remain in contact to continue the discussions, and foster new collaborations. There was strong enthusiasm for organising a follow-up Dagstuhl seminar in the future, perhaps taking place in about two years time. To enable future collaborations the participants:
- created a GitHub organisation where all seminar participants (and other researchers invited later) can exchange references and materials;
- agreed to use the seminar's Zulip chat (mentioned above) as a starting point to set up a more permanent solution for continuing the interactions and exchanges (e.g., a mailing list);
- nominated four people who will propose a new seminar, building upon the results of this one.
- Marco Carbone (IT University of Copenhagen, DK) [dblp]
- Simon Fowler (University of Glasgow, GB) [dblp]
- Philipp Haller (KTH Royal Institute of Technology - Kista, SE) [dblp]
- Mathias Jakobsen (University of Glasgow, GB) [dblp]
- Eduard Kamburjan (University of Oslo, NO) [dblp]
- Roland Kuhn (Actyx AG - München, DE) [dblp]
- Sam Lindley (University of Edinburgh, GB) [dblp]
- Fabrizio Montesi (University of Southern Denmark - Odense, DK) [dblp]
- Philip Munksgaard (University of Copenhagen, DK) [dblp]
- Alceste Scalas (Technical University of Denmark - Lyngby, DK) [dblp]
- Peter Thiemann (Universität Freiburg, DE) [dblp]
- Emilio Tuosto (Gran Sasso Science Institute, IT) [dblp]
- Gul Agha (University of Illinois - Urbana-Champaign, US) [dblp]
- Stephanie Balzer (Carnegie Mellon University - Pittsburgh, US) [dblp]
- Christian Bartolo Burló (Gran Sasso Science Institute, IT) [dblp]
- Laura Bocchi (University of Kent - Canterbury, GB) [dblp]
- Edwin Brady (University of St Andrews, GB) [dblp]
- Ilaria Castellani (INRIA - Sophia Antipolis, FR) [dblp]
- Tzu-Chun Chen (Evonik Industries - Hanau, DE) [dblp]
- Ornela Dardha (University of Glasgow, GB) [dblp]
- Mariangiola Dezani (University of Turin, IT) [dblp]
- Simon Gay (University of Glasgow, GB) [dblp]
- Raymond Hu (Queen Mary University of London, GB) [dblp]
- Atsushi Igarashi (Kyoto University, JP) [dblp]
- Jules Jacobs (Radboud University Nijmegen, NL) [dblp]
- Wen Kokke (University of Edinburgh, GB) [dblp]
- Dimitrios Kouzapas (University of Cyprus - Nicosia, CY) [dblp]
- Hernán Melgratti (University of Buenos Aires, AR) [dblp]
- J. Garrett Morris (University of Iowa - Iowa City, US) [dblp]
- Rumyana Neykova (Brunel University - Uxbridge, GB) [dblp]
- Marco Peressotti (University of Southern Denmark - Odense, DK) [dblp]
- Jorge Pérez (University of Groningen, NL) [dblp]
- Claudio Russo (Dfinity - Cambridge, GB) [dblp]
- Guido Salvaneschi (Universität St. Gallen, CH) [dblp]
- Bernardo Toninho (NOVA School of Science and Technology - Lisbon, PT) [dblp]
- Vasco T. Vasconcelos (University of Lisbon, PT) [dblp]
- Laura Voinea (University of Kent - Canterbury, GB) [dblp]
- Philip Wadler (University of Edinburgh, GB) [dblp]
- Nobuko Yoshida (Imperial College London, GB) [dblp]
- Fangyi Zhou (Imperial College London, GB) [dblp]
Verwandte Seminare
- Dagstuhl-Seminar 17051: Theory and Applications of Behavioural Types (2017-01-29 - 2017-02-03) (Details)
- Dagstuhl-Seminar 24051: Next Generation Protocols for Heterogeneous Systems (2024-01-28 - 2024-02-02) (Details)
- Dagstuhl-Seminar 26071: Behavioural Types for Resilience (2026-02-08 - 2026-02-13) (Details)
Klassifikation
- Logic in Computer Science
- Programming Languages
- Software Engineering
Schlagworte
- concurrency
- behavioural types
- session types
- programming languages