Return-Path: <John.Harrison-request@cl.cam.ac.uk>
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, 10 May 1993 18:34:59 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA05454;
          Mon, 10 May 93 10:17:40 -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 AA05449;
          Mon, 10 May 93 10:17:02 -0700
Received: from razorbill.cl.cam.ac.uk (user jg (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Mon, 10 May 1993 18:15:49 +0100
To: Mike Coe <coe@panther.cs.uidaho.edu>
Cc: info-hol@ted.cs.uidaho.edu
Subject: Re: wp and Hoare logic
In-Reply-To: Your message of Mon, 10 May 93 09:38:01 -0700. <199305101638.AA19935@panther.cs.uidaho.edu>
Date: Mon, 10 May 93 18:15:39 +0100
From: Jim Grundy <Jim.Grundy@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:029000:930510171553"@cl.cam.ac.uk>


> Does anyone have references to the 
> mechanizing of Dijkstra's wp calculus and
> Hoare's logic of triples

@MASTERSTHESIS{Age92a,
    author      = "Sten Agerholm",
    title       = "Mechanizing Program Verification in HOL",
    school      = "Computer Science Department, Matematisk Institut,
                    {\AA}rhus Universitet",
    address     = "Ny Munkegade, Building 540, DK-8000 {\AA}rhus C, Denmark",
    year        = 1992,
    month       = apr}

@ARTICLE{Bac90a,
    author      = "Ralph-Johan R. Back and Joakim von Wright",
    title       = "Refinement Concepts Formalised in Higher-Order Logic",
    journal     = "Formal Aspects of Computing",
    year        = 1990,
    volume      = 2,
    number      = 3,
    month       = jul,
    pages       = "247--272"}

@INPROCEEDINGS{Gor88a,
    author      = "Michael J. C. Gordon",
    title       = "Mechanizing Programming Logics in Higher-Order Logic",
    booktitle   = "Current Trends in Hardware Verification and
                    Automated Theorem Proving
                    ({P}roceedings of the 1988 Banff Workshop on
                    Hardware Verification)",
    editor      = "Graham M. Birtwistle and P. A. Subrahmanyam",
    chapter     = 10,
    year        = 1988,
    pages       = "387--439",
    publisher   = "Springer-Verlag, Berlin, Germany",
    address     = "Banff, Canada"}

@INPROCEEDINGS{Gru92a,
    author      = "Jim Grundy",
    title       = "A Window Inference Tool for Refinement",
    pages       = "230--254",
    editor      = "Cliff B. Jones and B. Tim Denvir and Roger C. F. Shaw",
    booktitle   = "Proceedings of the 5th Refinement Workshop",
    series      = "Workshops in Computer Science,
    address     = "Lloyd's Register, London, England",
    month       = "8--10 " # jan,
    year        = 1992,
    organization= "BCS-FACS",
    publisher   = "Springer-Verlag, London, England"}

Jim