Simon Fowler (University of Glasgow) |
Philipp Haller (Digital Futures, KTH Royal Institute of Technology) |
Roland Kuhn (Actyx AG) |
Sam Lindley (The University of Edinburgh) |
Alceste Scalas (Technical University of Denmark) |
Vasco T. Vasconcelos (University of Lisbon) |
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. |
ArXived at: https://dx.doi.org/10.4204/EPTCS.401.4 | bibtex | |
Comments and questions to: eptcs@eptcs.org |
For website issues: webmaster@eptcs.org |