Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) outside ac.uk; Tue, 23 Feb 1993 16:55:46 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA15160; Tue, 23 Feb 93 08:31:54 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA15045; Tue, 23 Feb 93 08:27:06 -0800 Received: from guillemot.cl.cam.ac.uk (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) to cl; Tue, 23 Feb 1993 16:25:58 +0000 To: cjoosse@fi.abo.ra (Carine Joosse INF) Cc: info-hol@edu.uidaho.cs.ted, Tom.Melham@uk.ac.cam.cl In-Reply-To: Your message of Tue, 23 Feb 93 11:37:16 +0200. <9302230937.AA20603@ra.abo.fi> Date: Tue, 23 Feb 93 16:25:52 +0000 From: Tom Melham Message-Id: <"swan.cl.ca.833:23.02.93.16.26.01"@cl.cam.ac.uk> > I am working with hol, in particular programming logic, > (files in /prog_logic88) but am having some difficulties. > Who can help me? I want to know where I can find some > proper documentation about the programming and specification > languages for the programs that are provable using for instance > hoare-logic, also some examples might be helpful (I can only > find numerous versions of a division program and some out- > dated documentation). The theory behind prog_logic88 is documented in the following paper: M. J. C. Gordon, `Mechanizing Programming Logics in Higher Order Logic', in Current Trends in Hardware Verification and Automated Theorem Proving, edited by G. Birtwistle and P. A. Subrahmanyam (Springer-Verlag, 1989), pp. 387-439. This is also available as Technical Report number 145 from the University of Cambridge Computer Laboratory. For general background and lots of examples, see Mike's Gordon's Book: M. J. C. Gordon, Programming Language Theory and its Implementation, Prentice-Hall International Series in Computer Science (Prentice-Hall, 1988). Tom