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 17:57:15 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA05395;
          Mon, 10 May 93 09:37:57 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from panther.cs.uidaho.edu by ted.cs.uidaho.edu (16.6/1.34) 
          id AA05390; Mon, 10 May 93 09:37:52 -0700
Received: by panther.cs.uidaho.edu id AA19935 (5.65c/IDA-1.4.4 
          for info-hol@ted); Mon, 10 May 1993 09:38:02 -0700
From: Mike Coe <coe@panther.cs.uidaho.edu>
Message-Id: <199305101638.AA19935@panther.cs.uidaho.edu>
Subject: wp and Hoare logic
To: info-hol@ted.cs.uidaho.edu
Date: Mon, 10 May 93 9:38:01 PDT
X-Mailer: ELM [version 2.3 PL11]



Does anyone have references to the 
mechanizing of Dijkstra's wp calculus and
Hoare's logic of triples.  I have the monograph
by  Gavan Tredoux about how he embedded these
into the HOL logic by using execution sequences.


I would be interested in other examples such as this
for HOL or any other theorem prover.


thanks,,


mike