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; Wed, 19 May 1993 09:44:35 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA28342;
          Wed, 19 May 93 01:28:28 -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 AA28337;
          Wed, 19 May 93 01:28:22 -0700
Received: from coot.cl.cam.ac.uk (user pc (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Wed, 19 May 1993 09:28:03 +0100
To: Mike Coe <coe@panther.cs.uidaho.edu>
Cc: info-hol@ted.cs.uidaho.edu, Paul.Curzon@cl.cam.ac.uk
Subject: Re: wp and Hoare logic
In-Reply-To: Your message of "Mon, 10 May 93 09:38:01 PDT." <199305101638.AA19935@panther.cs.uidaho.edu>
Date: Wed, 19 May 93 09:27:56 +0100
From: Paul Curzon <Paul.Curzon@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:053420:930519082813"@cl.cam.ac.uk>


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


I mechanized a Hoare logic in HOL for the Vista language and
combined it with a compiler correctness theorem for the language.
This allowed correctness theorems to be proved about source programs
using the Hoare logic, and then corresponding correctness theorems
to be automatically obtained about the object code. References below.

Paul Curzon.
(pc@cl.cam.ac.uk)
------------------

@InProceedings{Curzon92LPAR,
  author = 	"Paul Curzon",
  title = 	"A Programming Logic For a Verified Structured Assembly Language",
  booktitle = 	"Logic Programming and Automated Reasoning",
  year = 	"1992",
  editor = 	"A. Voronkov",
  pages = 	"403-408",
  publisher = 	"Springer-Verlag",
  volume = 	"624",
  series = 	"Lecture Notes in Artificial Intelligence",
}


@InProceedings{Curzon92HOL,
  author = 	"Paul Curzon",
  title = 	"Deriving Correctness Properties of Compiled Code",
  booktitle = 	"Proceedings of the International Workshop on Higher Order Logic
                 Theorem Proving and its Applications",
  year = 	"1993",
  editor = 	"L. Claesen and M. Gordon",
  publisher = 	"North-Holland",
  series = 	"{IFIP} Transactions {A}-20",
}


@Unpublished{Curzon93FMSD,
  author = 	"Paul Curzon",
  title = 	"Deriving Correctness Properties of Compiled Code",
  note = 	"To appear in {\em Formal Methods in System Design}, Kluwer,
                 (an extended version of the above)",
}