Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 16 Jun 1994 16:03:21 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA23365; Thu, 16 Jun 1994 08:49:59 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA23361; Thu, 16 Jun 1994 08:49:56 -0600 Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) id AA20063; Thu, 16 Jun 1994 07:48:17 -0700 Received: from albatross.cl.cam.ac.uk (user adg (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Thu, 16 Jun 1994 15:47:28 +0100 To: info-hol@cs.uidaho.edu Subject: Re: Information on uses of HOL for software verification In-Reply-To: Your message of "Wed, 15 Jun 94 11:54:00 +0930." <9406150224.AA16804@itd0.dsto.gov.au> Date: Thu, 16 Jun 94 15:47:21 +0100 From: Andrew Gordon Message-Id: <"swan.cl.cam.:062090:940616144742"@cl.cam.ac.uk> Jim wrote: >the construction of a nontrivial, >real-world, verified application using HOL, I'm not sure that such a beast >exists, please let me know if you find one I'm not sure if he's written it up yet, but I was impressed by a recent seminar in which Joachim von Wright described his work on a verified imperative program that checks HOL proofs. To address Jim's list, its nontrivial (50 subroutines), verified in HOL and, OK, it's not real-world in the same sense as the flight control program for the Airbus, but on the other hand it's not the figment of anybody's imagination! If you're reading this, Joachim, maybe you could fill in more details. Andy.