[Prev][Next][Index][Thread]
Tech report: `A theory of weak bisimulation for core CML'
We are pleased to announce the availablility of a technical report:
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:
ftp://ftp.cogs.susx.ac.uk/pub/reports/compsci/cs0595.ps.Z
All reports from the School are available from:
http://www.cogs.susx.ac.uk/reports.html
Alan.
--
Alan Jeffrey Tel: +44 1273 678526 alanje@cogs.susx.ac.uk
School of Cognitive and Computing Sciences, Sussex Univ., Brighton BN1 9QH, UK