Anna Ingolfsdottir - Towards Verified Lazy Implementation of Concurrent Value-Passing Languages
The behaviour of concurrent processes with value-passing is typically described by means of labelled transition systems. These semantic descriptions are, in general, on a very abstract level and implementation details, such as how the values are actually transmitted from one process to another, are not considered. In this paper we will give a more concrete semantic model, based on the ``lazy''-approach, for (the late-version of) the standard CCS where the exchange of data takes place by means of synchronized use of a common store. We also prove the ``correctness'' of this ``implementation'', i.e. we prove that this new semantics corresponds to the standard one in some formal but intuitive sense.