Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) outside ac.uk; Tue, 9 Mar 1993 18:14:01 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA02767; Tue, 9 Mar 93 09:50:12 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from panther.cs.uidaho.edu by ted.cs.uidaho.edu (16.6/1.34) id AA02762; Tue, 9 Mar 93 09:50:08 -0800 Received: from localhost by panther.cs.uidaho.edu with SMTP id AA04493 (5.65c/IDA-1.4.4 for info-hol@cs.uidaho.edu); Tue, 9 Mar 1993 08:09:33 -0800 Message-Id: <199303091609.AA04493@panther.cs.uidaho.edu> To: info-hol@edu.uidaho.cs.ted Subject: Re: Constructive logic, Nuprl and Hardware Verification Date: Tue, 09 Mar 93 08:09:32 -0800 From: Phil Windley X-Mts: smtp On Fri, 05 Mar 93 20:56:50 EST, mel@ultrastar.EE.CORNELL.EDU wrote: +------------ | In the HOL workshop last September, Mark Aagaard and I had a paper | discussing how to exploit Nuprl's type theory to support multiple | hardware implementations of the same specification. This work could | be done in HOL. We believe that this would essentially require | duplicating the support of dependent types in HOL. Indeed has been. I came home from the HOL workshop and used my abstract theory package (ATP) to implement the functions that Mark talked about. You don't really need dependent type to duplicate what Mark and Miriam did, but you do need subtypes (Miriam concurs here). The ATP does subtypes, but not dependent types. The place that I wish most for dependent types is in formulating vectors, particularly vectors of bits. From what Mark and Miriam tell me, they have found NUPRL's dependent type mechanism helpful in describing vectors. I remember a very nice talk by Keith Hanna at the second HOL workshop on VERITAS and how he formulated n-bit words. Does anyone have a copy of his slides by any chance? --phil--