An algebra of behavioural types (Q418153)

The paper is concerned with type systems for concurrent objects. Typically, a type system is a set of axioms and inference rules which act as an abstract proof system aimed at guaranteeing, for example, that a function is always called with the right number of arguments. In the case of concurrent objects, static typing with interfaces-as-types is not sufficient when it comes to dealing with dynamic changes of the interface (the set of currently enabled methods). To address this problem, the paper introduces the simple algebra of behavioural types (ABT), inspired by CCS-like process algebraic models. ADT terms are meant to characterise life cycles of concurrent objects. As the corresponding states represent changing interfaces, such terms describe sequences of methods being offered, and can be used for typing concurrent objects as well as reasoning about their behavioural correctness. The development of ADT induces in a natural way a novel notion of behavioural equivalence which is investigated in depth. In particular, the paper proposes its axiomatisation which is shown to be sound for general terms, and also complete in the case of a sublanguage of sequential image-finite expressions.