@ARTICLE{PittsAM:procbu,
AUTHOR = {A.~M.~Pitts and J.~R.~X.~Ross},
TITLE = {Process Calculus Based Upon Evaluation to Committed Form},
JOURNAL = {Theoretical Computer Science},
VOLUME= 195,
YEAR = 1998,
PAGES = {155--182},
NOTE = {A preliminary version of this paper appeared in
CONCUR'96, Lecture Notes in Computer Science Vol.~1119
(Springer-Verlag, Berlin, 1996), pp~18--33},
ABSRACT={An approach to the semantics of CCS-like communicating
processes is proposed that is based upon evaluation of processes to
input- or output-committed form, with no explicit mention of silent
actions. This leads to a co-inductively defined notion of
evaluation bisimilarity---a form of weak branching-time
equivalence which is shown to be a congruence, even in the presence of
summation. The relationship between this evaluation-based approach
and the more traditional, labelled transition semantics is
investigated. In particular, with some restriction on sums, CCS
observation equivalence is characterised purely in terms of evaluation
to committed form, and evaluation bisimilarity is characterised as a
weak delay equivalence. These results are extended to the higher
order case, where evaluation bisimilarity coincides with Sangiorgi's
weak context bisimilarity. An evaluation-based approach to
pi-calculus and the relationship with Milner and Sangiorgi's
reduction-based notion of barbed bisimulation are also examined.}
}