[LF] ================================================ AMAST Links 02 07

              A theory of weak bisimulation for core CML
                W. Ferreira, M. Hennessy and A. Jeffrey

  Concurrent ML is an extension of Standard ML of New Jersey with
concurrent features similar to those of process algebra. Reppy has
given it an operational semantics based on reductions of
configurations, using entire programs rather than program
fragments. The existing semantics are not, therefore compositional,
and do not support compositional reasoning (for example equational
reasoning about program fragments). 
  We present a compositional operational semantics for a fragment of
CML, based on higher-order process algebra, and use this to define
weak bisimulation for CML. We give some small examples of proofs about
CML expressions and show that our semantics corresponds to Reppy's up
to weak first-order bisimulation.
  Computer Science Technical Report 95:05, School of Cognitive and
Computing Sciences, University of Sussex. 
  The report is available electronically from URL:
ftp://ftp.cogs.susx.ac.uk/pub/reports/compsci/cs0595.ps.Z
  All _reports_ from the School are available from URL:
http://www.cogs.susx.ac.uk/reports.html