Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4); Tue, 19 Jan 1993 19:20:46 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA11841;
          Tue, 19 Jan 93 11:06:28 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA11836;
          Tue, 19 Jan 93 11:06:18 -0800
Received: from fulmar.cl.cam.ac.uk (user mn (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) to cl; Tue, 19 Jan 1993 19:05:33 +0000
To: info-hol@edu.uidaho.cs.ted
Subject: Technical Report available by ftp
Date: Tue, 19 Jan 93 19:05:23 +0000
From: Monica Nesi <Monica.Nesi@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.459:19.01.93.19.05.41"@cl.cam.ac.uk>



The following paper is now available by ftp from ftp.cl.cam.ac.uk in the
directory hvg/papers. It is in the file CCSinHOL.ps.Z. It has appeared as 
University of Cambridge, Computer Laboratory Technical Report Number 278.

  A Formalization of the Process Algebra CCS in Higher Order Logic

  Monica Nesi

  This paper describes a mechanization in higher order logic of the theory
  for a subset of Milner's CCS. The aim is to build a sound and effective tool
  to support verification and reasoning about process algebra specifications.
  To achieve this goal, the formal theory for pure CCS (no value passing)
  is defined in the interactive theorem prover HOL, and a set of proof tools,
  based on the algebraic presentation of CCS, is provided.


Monica