Return-Path: Delivery-Date: Received: from cs.uidaho.edu (actually ted.cs.uidaho.edu !OR! info-hol-request@cs.uidaho.edu) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 8 Jul 1993 13:16:58 +0100 Received: by cs.uidaho.edu (16.6/2.0) id AA26536; Thu, 8 Jul 93 05:09:10 -0700 Sender: info-hol-request@cs.uidaho.edu Errors-To: info-hol-request@cs.uidaho.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by cs.uidaho.edu (16.6/2.0) id AA26531; Thu, 8 Jul 93 05:09:03 -0700 Received: from guillemot.cl.cam.ac.uk (user tfm (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Thu, 8 Jul 1993 13:09:16 +0100 To: info-hol@cs.uidaho.edu Cc: Tom.Melham@cl.cam.ac.uk Subject: Camb. technical reports by ftp. Date: Thu, 08 Jul 93 13:09:12 +0100 From: Tom Melham Message-Id: <"swan.cl.cam.:295880:930708120924"@cl.cam.ac.uk> Regarding the correspondence about tech reports: > Sorry if this is a stupid question. Is there > an ftp site for tech reports from > Cambridge University--and not just recent ones.. ... > Not that I know of. The FTP site |ftp.cl.cam.ac.uk| has two directories for > papers and reports: > ... > ... It would be desirable to add some of the old techreports to the FTP > area, but this depends on their authors still having the source and being > prepared to get it all working and install it. Many might regard their old > reports as obselete anyway! I'll get things started by installing my technical report on defining the pi-calculus in HOL. The index entry is attached. I'll try to install other "old" tech reports as well. Tom =====================================================================. * PIinHOL.ps.Z PIinHOL.dvi.Z A Mechanized Theory of the pi-calculus in HOL T. F. Melham Technical Report No. 244, University of Cambridge Computer Laboratory (January 1992). The pi-calculus is a process algebra developed at Edinburgh by Milner, Parrow and Walker for modelling concurrent systems in which the pattern of communication between processes may change over time. This paper describes the results of preliminary work on a mechanized formal theory of the pi-calculus in higher order logic using the HOL theorem prover.