Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Tue, 8 Jun 1993 22:05:00 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA09183; Tue, 8 Jun 93 13:54:38 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from grolsch.cs.ubc.ca by ted.cs.uidaho.edu (16.6/1.34) id AA09178; Tue, 8 Jun 93 13:54:33 -0700 Received: by grolsch.cs.ubc.ca id AA05395 (5.65c/IDA-1.3.5 for info-hol@ted.cs.uidaho.edu); Tue, 8 Jun 1993 13:54:52 -0700 Date: 8 Jun 93 13:54 -0700 From: Jeffrey Joyce To: info-hol Message-Id: <7017*joyce@cs.ubc.ca> Subject: Parnas: "some theorems we should prove" Dave Parnas has submitted a paper to HUG'93 on "Some Theorems we Should Prove" which gives examples of theorems that would be useful to prove in the context of producing precise, provably complete documentation for computer systems. With his permission, we have made a draft version of this paper available by anonymous ftp as: cs.ubc.ca:/ftp/local/hug93/parnas.ps.Z This paper is being made available to motivate some investigation into the ease/difficulty of proving such theorems using HOL and other theorem-proving systems. In particular, we would welcome short (2-3 pages) summaries of such investigations. These summaries should give an account of the overall amount of effort to prove the theorems outlined by Parnas, i.e., we are more interested in the fact that it took two days for you to set up the problem than the fact that your completed proof script runs in 1.5 seconds on an XXX with 32M. Summaries should be sent to hug93@cs.ubc.ca before July 7 as camera-ready PostScript. We can't guarantee that there will be a time slot in the regular program for HUG'93 to discuss these summaries -- however, I expect that there will be some opportunities to informally discuss these summaries. The summaries will be distributed to workshop participants.