Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Mon, 31 May 1993 17:45:14 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA05110; Mon, 31 May 93 09:38:38 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA05105; Mon, 31 May 93 09:38:30 -0700 Received: from dipper.cl.cam.ac.uk (user mjcg (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Mon, 31 May 1993 17:38:07 +0100 Received: by dipper.cl.cam.ac.uk (4.1/SMI-3.0DEV3) id AA23496; Mon, 31 May 93 17:37:56 BST Date: Mon, 31 May 93 17:37:56 BST From: Mike.Gordon@cl.cam.ac.uk Message-Id: <9305311637.AA23496@dipper.cl.cam.ac.uk> To: info-hol@ted.cs.uidaho.edu Subject: Papers available by FTP A couple of new papers in the Cambridge FTP area: * HoareLogicPaper.ps.Z HoareLogicPaper.dvi.Z A mechanized Hoare Logic of state transitions Mike Gordon Companion paper to "State transition assertions: a case study" (also available by FTP). Describes a Hoare Logic for reasoning about data processing aspects of real time systems. Written for the Hoare Festschrift, to be edited by Bill Roscoe, Prentice-Hall, 1994. * HOLPaper.ps.Z HOLPaper.dvi.Z The HOL logic and system Mike Gordon Description of the syntax of the HOL logic and a brief overview of the theorem proving infrastructure. A chapter for the SAFEMOS book. Condensed from "Introduction to HOL" by Gordon and Melham.