Return-Path: Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <02782-0@swan.cl.cam.ac.uk>; Sat, 18 Jan 1992 03:02:34 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA03386; Fri, 17 Jan 92 18:49:48 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from ULTRASTAR.EE.CORNELL.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA03375; Fri, 17 Jan 92 18:49:36 -0800 Date: Fri, 17 Jan 92 21:51:47 -0500 From: markaa@EDU.CORNELL.EE.ultrastar (Mark D. Aagaard) Received: by ultrastar.EE.CORNELL.EDU (5.65+IDA-1.3.5+christos-1/1.6.10+n-y-Cornell-Electrical-Engineering) id AA26781; Fri, 17 Jan 92 21:51:47 -0500 Message-Id: <9201180251.AA26781@ultrastar.EE.CORNELL.EDU> To: info-hol@edu.uidaho.cs.ted Subject: verification of pipelines I am beginning to look at verifying pipelines in the Nuprl proof development system. If anyone knows of any previous work in pipeline verification (in HOL, any other system, or on paper) I would appreciate it they would send the references to me. If there is sufficient interest, I will mail any references that I collect to info-hol. Thanks, Mark Aagaard markaa@ee.cornell.edu 389 Engineering and Theory Center Cornell University Ithaca NY 14850