[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