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; Thu, 10 Aug 1995 09:23:13 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA206140765; Thu, 10 Aug 1995 01:46:05 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA206110763; Thu, 10 Aug 1995 01:46:03 -0600 Received: from woodcock.cl.cam.ac.uk (user mjcg (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Thu, 10 Aug 1995 08:46:00 +0100 Received: by woodcock.cl.cam.ac.uk (4.1/SMI-3.0DEV3) id AA14954; Thu, 10 Aug 95 08:45:50 BST Date: Thu, 10 Aug 95 08:45:50 BST From: Mike.Gordon@cl.cam.ac.uk Message-Id: <9508100745.AA14954@woodcock.cl.cam.ac.uk> To: info-hol@leopard.cs.byu.edu Subject: Notes on PVS from a HOL perspective During the first week of July I visited SRI Menlo Park to find out more about PVS. The preceding week I attended LICS95, where I had several talks with Shankar accompanied by demos of the system on his SparcBook laptop. I've written a note on some of the things I learned, together with a discussion of their implications for the evolution of the HOL system. This note is available over the WWW at the URL: http://www.cl.cam.ac.uk/users/mjcg/PVS.ps.gz Comments etc will be much appreciated. Mike