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

Dagstuhl Service Team

Documents

Dagstuhl Report, Volume 11, Issue 8 Dagstuhl Report
Aims & Scope
List of Participants
Dagstuhl Seminar Wiki
Dagstuhl Seminar Schedule [pdf]

(Use personal credentials as created in DOOR to log in)

Summary

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:

  1. created a GitHub organisation where all seminar participants (and other researchers invited later) can exchange references and materials;
  2. 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);
  3. nominated four people who will propose a new seminar, building upon the results of this one.
Summary text license
  Creative Commons BY 4.0
  Mariangiola Dezani, Roland Kuhn, Sam Lindley, and Alceste Scalas

Dagstuhl Seminar Series

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).

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.

Publications

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