Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: list
Message-Id: <199511241459.HAA05221@bunsen.cs.byu.edu>
To: Cardell-Oliver R <cardr@essex.ac.uk>
Cc: info-hol@cs.byu.edu, tfm@dcs.gla.ac.uk
Subject: Re: CSP in HOL 
In-Reply-To: Your message of "Fri, 24 Nov 1995 11:10:17 GMT."             <12781.9511241110@csc12.essex.ac.uk> 
Date: Fri, 24 Nov 1995 14:58:24 +0000
From: Tom Melham <tfm@dcs.gla.ac.uk>

> I am planning to embed the failures semantics of CSP in HOL.
> Has anyone done this in HOL, or Isabelle or ...? Can anyone
> supply any references to related work?  I know of Albert
> Camilleri's IEEE SE paper, but haven't yet seen anything else.

A quick search of my new HOL bibliography [1] reveals two papers:
  
  A. J. Camilleri, `A Higher Order Logic Mechanization of the CSP
  Failure-Divergence Semantics', in IV Higher Order Workshop, Banff 
  1990: Proceedings, edited by G. Birtwistle (Springer-Verlag, 1991), 
  pp. 123-150.

  A. J. Camilleri, `Mechanizing CSP Trace Theory in Higher Order Logic', 
  IEEE Transactions on Software Engineering, vol. 16, no. 9 (September, 
  1990), pp. 993-1004.

> The second (long term) goal, is to verify a link between
> non-deterministic sequential programs (with an operational
> semantics) and CSP (failures semantics).

The report done by Juan Camilleri and me

  Camilleri and T. Melham, `Reasoning with Inductively Defined Relations
  in the HOL Theorem Prover', Technical Report Number 265, University of
  Cambridge Computer Laboratory (August 1992). 

has a little example that's (rather distantly) related to this.

Tom

[1] http://www.dcs.glasgow.ac.uk/~tfm/hol-bib.html