Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Wed, 1 Mar 1995 15:44:48 +0000
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA234911329;
          Wed, 1 Mar 1995 08:22:09 -0700
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu 
          with ESMTP (1.37.109.15/16.2) id AA234721278;
          Wed, 1 Mar 1995 08:21:18 -0700
Received: from puffin.cl.cam.ac.uk (user btg (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Wed, 1 Mar 1995 15:19:18 +0000
To: rahard@ee.UManitoba.CA
Cc: info-hol@leopard.cs.byu.edu
Subject: Re: Mechanizing CSP
In-Reply-To: Your message of "Wed, 01 Mar 1995 08:00:43 CST." <9503011400.AA27355@ic14.ee.umanitoba.ca>
Date: Wed, 01 Mar 1995 15:19:12 +0000
From: Brian Graham <Brian.Graham@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:056740:950301151923"@cl.cam.ac.uk>

<rahard@ee.UManitoba.CA> wrote:

> I am reading A.J. Camilleri, "Mechanizing CSP Trace Theory in
> Higher Order Logic," IEEE Trans. on Software Eng., vol 16, no. 9,
> pp. 993--1004, Sept 1990.

> Is there a package/theory available for this?
> Is there related/newer HOL references/package/theory related to CSP?

Look in contrib/CSP.  It is available both in hol88 and hol90.7.

--brian