Behavioural Prototypes
Roly Perera, Simon J. Gay

TL;DR
This paper introduces a language of concurrent objects that combines type system principles with continuous testing to ensure communication compatibility and prevent runtime errors in concurrent programs.
Contribution
It presents a novel language framework that applies session type concepts to terms, enabling automatic compatibility checks for concurrent objects.
Findings
Programs are collections of communicating automata.
Automated checks guarantee multiparty compatibility.
No runtime message-related errors occur.
Abstract
We sketch a simple language of concurrent objects which explores the design space between type systems and continuous testing. In our language, programs are collections of communicating automata checked automatically for multiparty compatibility. This property, taken from the session types literature but here applied to terms rather than types, guarantees that no state-related errors arise during execution: no object gets stuck because it was sent the wrong message, and every message is processed.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Parallel Computing and Optimization Techniques
