Emerging interaction paradigms, such as service-oriented computing, and new technological challenges, such as exogenous component coordination, suggest new roles and application areas for process algebras. This, however, entails the need for more generic and adaptable approaches to their design. For example, some applications may require similar programming constructs coexisting with different interaction disciplines. In such a context, this paper pursues a research programme on a coinductive rephrasal of classic process algebra, proposing a clear separation between structural aspects and interaction disciplines. A particular emphasis is put on the study of interruption combinators defined by natural co-recursion. The paper also illustrates the verification of their properties in an equational and pointfree reasoning style as well as their direct encoding in Haskell.

Process Algebra, coinduction, coalgebra