Received: from leopard.cs.byu.edu (leopard.cs.byu.edu [128.187.2.182]) by ra.abo.fi (8.6.10/8.6.10) with ESMTP id OAA18597; Fri, 24 Nov 1995 14:38:49 +0200
Received: by leopard.cs.byu.edu
	(1.37.109.15/16.2) id AA290871669; Fri, 24 Nov 1995 04:14:29 -0700
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: list
Received: from bunsen.cs.byu.edu by leopard.cs.byu.edu with ESMTP
	(1.37.109.15/16.2) id AA290731606; Fri, 24 Nov 1995 04:13:26 -0700
Received: from postman.essex.ac.uk (postman.essex.ac.uk [155.245.10.14]) 
  by bunsen.cs.byu.edu (8.6.9/8.6.9) with SMTP
  id EAA04470 for <info-hol@cs.byu.edu>; Fri, 24 Nov 1995 04:11:38 -0700
Received: from postman.essex.ac.uk by postman.essex.ac.uk with SMTP (PP) 
          id <02480-0@postman.essex.ac.uk>; Fri, 24 Nov 1995 11:10:17 +0000
From: Cardell-Oliver R <cardr@essex.ac.uk>
Date: Fri, 24 Nov 95 11:10:17 GMT
Message-Id: <12781.9511241110@csc12.essex.ac.uk>
To: info-hol@cs.byu.edu
Subject: CSP in HOL



I am planning to embed the failures semantics of CSP in HOL.
Well ... I've started thinking about it.
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.
Advice of the form "I thought about doing it but decided it
was a mad idea" (with reasons) would be useful too!

I have two applications in mind. 
The first is to prove some satisfaction properties for given
processes and specifications using the compositional 
laws for parallelism and concealment (p124 and 125 of Hoare's 
book), and some reasoning about traces and their prefixes and
about refusal sets.
The second (long term) goal, is to verify a link between
non-deterministic sequential programs (with an operational
semantics) and CSP (failures semantics).
In both cases I have (someone elses) hand proofs to start with, 
although for the second case the proof is just an outline.

Thanks,
Rachel