Behavioural Prototypes

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.