Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Mon, 22 Nov 1993 14:59:44 +0000 Received: by leopard.cs.byu.edu (1.37.109.7/16.2) id AA18440; Mon, 22 Nov 93 07:28:09 -0700 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.cs.byu.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with SMTP (1.37.109.7/16.2) id AA18436; Mon, 22 Nov 93 07:24:07 -0700 Received: from fulmar.cl.cam.ac.uk (user mn (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Mon, 22 Nov 1993 14:19:33 +0000 To: Matthias Mutz Cc: info-hol@leopard.cs.byu.edu, Monica.Nesi@cl.cam.ac.uk Subject: Re: mechanization of CCS In-Reply-To: Your message of "Mon, 22 Nov 93 13:23:30 +0100." <199311221224.AA02041@kirk.fmi.uni-passau.de> Date: Mon, 22 Nov 93 14:19:14 +0000 From: Monica Nesi Message-Id: <"swan.cl.cam.:283920:931122141950"@cl.cam.ac.uk> Hi Matthias, I have been working on mechanizing CCS in HOL in the framework of my thesis. Pure CCS (no value passing) has been formalized in HOL and you can find a report on this work in a technical report available via ftp, as said in the attached message. I'm currently working on formalizing value-passing CCS and the up-to-date report on this work is the paper "Value-Passing CCS in HOL" that I presented at the HUG93 workshop in Vancouver. I can send you the revised version of this paper, if you like. Monica ************ To: info-hol@ted.cs.uidaho.edu Subject: Technical Report available by ftp Date: Tue, 19 Jan 93 19:05:23 +0000 From: Monica Nesi 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 ************ ------------------------------------------------------------------------------ Monica Nesi | Tel: +44-223-334733 University of Cambridge | Fax: +44-223-334678 Computer Laboratory | New Museums Site | Email: mn@cl.cam.ac.uk Pembroke Street | Cambridge CB2 3QG | England | ------------------------------------------------------------------------------