Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
427058 | Information and Computation | 2012 | 28 Pages |
Abstract
We propose a process algebra, the Algebra of Behavioural Types, as a language for typing concurrent objects. A type is a higher-order labelled transition system that characterises all possible life cycles of a concurrent object. States represent interfaces of objects; state transitions model the dynamic change of object interfaces. Moreover, a type provides an internal view of the objects that inhabits it: a synchronous one, since transitions correspond to message reception. To capture this internal view of objects we define a notion of bisimulation, strong on labels and weak on silent actions. We study several algebraic laws that characterise this equivalence, and obtain completeness results for image-finite types.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics