Towards Verified Lazy Implementation of Concurrent Value-Passing Languages

 Anna Ingolfsdottir1, Rosario Pugliese2
1 BRICS, Dept. of Computer Science, Aalborg University
2 Dipartimento di Sistemi e Informatica, Universita' di Firenze


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. 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.