Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Behavioural Types for Heterogeneous Systems (Position Paper)

Simon Fowler, Philipp Haller, Roland Kuhn, Sam Lindley, Alceste Scalas, Vasco T. Vasconcelos

TL;DR

The paper tackles the barrier to adopting behavioural types in real-world, heterogeneous software by proposing a modular architecture that decouples protocol specification from language-specific implementations. It introduces an extensible protocol description language, a session intermediate representation (Session IR) to capture monitoring, data transformations, and boundary handling, and session proxies to bridge components across languages. The approach aims to preserve safety properties of MPSTs while accommodating timing constraints and data refinements across heterogeneous components. It also discusses potential challenges, including ensuring safe composition of extensions, managing runtime overhead, and establishing a workable metatheory, thereby stimulating discussion on practical adoption of behavioural typing in diverse software ecosystems.

Abstract

Behavioural types provide a promising way to achieve lightweight, language-integrated verification for communication-centric software. However, a large barrier to the adoption of behavioural types is that the current state of the art expects software to be written using the same tools and typing discipline throughout a system, and has little support for components over which a developer has no control. This position paper describes the outcomes of a working group discussion at Dagstuhl Seminar 24051 (Next-Generation Protocols for Heterogeneous Systems). We propose a methodology for integrating multiple behaviourally-typed components, written in different languages. Our proposed approach involves an extensible protocol description language, a session IR that can describe data transformations and boundary monitoring and which can be compiled into program-specific session proxies, and finally a session middleware to aid session establishment. We hope that this position paper will stimulate discussion on one of the most pressing challenges facing the widespread adoption of behavioural typing.

Behavioural Types for Heterogeneous Systems (Position Paper)

TL;DR

The paper tackles the barrier to adopting behavioural types in real-world, heterogeneous software by proposing a modular architecture that decouples protocol specification from language-specific implementations. It introduces an extensible protocol description language, a session intermediate representation (Session IR) to capture monitoring, data transformations, and boundary handling, and session proxies to bridge components across languages. The approach aims to preserve safety properties of MPSTs while accommodating timing constraints and data refinements across heterogeneous components. It also discusses potential challenges, including ensuring safe composition of extensions, managing runtime overhead, and establishing a workable metatheory, thereby stimulating discussion on practical adoption of behavioural typing in diverse software ecosystems.

Abstract

Behavioural types provide a promising way to achieve lightweight, language-integrated verification for communication-centric software. However, a large barrier to the adoption of behavioural types is that the current state of the art expects software to be written using the same tools and typing discipline throughout a system, and has little support for components over which a developer has no control. This position paper describes the outcomes of a working group discussion at Dagstuhl Seminar 24051 (Next-Generation Protocols for Heterogeneous Systems). We propose a methodology for integrating multiple behaviourally-typed components, written in different languages. Our proposed approach involves an extensible protocol description language, a session IR that can describe data transformations and boundary monitoring and which can be compiled into program-specific session proxies, and finally a session middleware to aid session establishment. We hope that this position paper will stimulate discussion on one of the most pressing challenges facing the widespread adoption of behavioural typing.
Paper Structure (11 sections, 3 equations, 1 figure)

This paper contains 11 sections, 3 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Paper structure.
  3. Background
  4. (Multiparty) Session Types.
  5. Runtime Monitoring against Session Types.
  6. Multi-language Interoperability.
  7. Heterogeneous Multiparty Session Typing
  8. Proposed Solution
  9. Potential Challenges
  10. Related Work
  11. Conclusion

Figures (1)

  • Figure 1: Proposed System