Return-Path:
Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0)
          id <07866-0@swan.cl.cam.ac.uk>; Tue, 4 Feb 1992 12:35:00 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA03233;
          Tue, 4 Feb 92 04:15:10 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA03229;
          Tue, 4 Feb 92 04:15:05 -0800
Received: from guillemot.cl.cam.ac.uk by swan.cl.cam.ac.uk
          with SMTP (PP-6.0) to cl id <06939-0@swan.cl.cam.ac.uk>;
          Tue, 4 Feb 1992 12:02:43 +0000
To: info-hol@edu.uidaho.cs.ted
Cc: Tom.Melham@uk.ac.cam.cl
Subject: Technical Report available.
Date: Tue, 04 Feb 92 12:02:05 +0000
From: Tom.Melham@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.969:04.01.92.12.03.29"@cl.cam.ac.uk>


For those of you interested in embedding languages in HOL, there is
finally a technical report available on the pi-calculus work that I
spoke about at the HOL user's meeting in Aarhus.  If you are interested
in a copy, please let me know and I'll send you one.  The abstract is,
I'm afraid, not particularly informative, but here it is:

      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.

Tom