A behavioural theory of first-order CML

AbstractWe investigate a number of semantic issues which arise, when a language of expressions such as ML, is augmented with constructs for communication and concurrency, as is the case with CML. We construct a simple language of first-order expressions, which includes an operator let… = …in…end to provide a form of sequentialisation and a simple form of abstraction, communication constructs, and a spawn operator, for expressing concurrency. We construct an operational semantics for the language, which ensures that a number of natural laws for the let operator hold. In addition we provide a testing semantics for the language, and show how a fully abstract model for the resulting testing preorder, can be constructed from a variation of Acceptance Trees