Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
To: Phil Windley <windley@edu.uidaho.cs.panther>
Cc: info-hol@edu.uidaho.cs.ted, Tom.Melham@uk.ac.cam.cl
Subject: Re: Constructive logic, Nuprl and Hardware Verification
In-Reply-To: Your message of Tue, 09 Mar 93 08:09:32 -0800. <199303091609.AA04493@panther.cs.uidaho.edu>
Date: Tue, 09 Mar 93 18:31:31 +0000
From: Tom Melham <Tom.Melham@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.683:09.03.93.18.31.42"@cl.cam.ac.uk>


Further to Phil's message:

> 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?

I would add that Bart Jacobs and I have an implementation of dependent type
theory in HOL.  Please accept my apologies for announcing this twice, but 
see the paper DTTinHOL.ps.Z at ftp.cl.cam.ac.uk in the directory /hvg/papers.

Anyone interested in using (or otherwise playing with) the HOL code that
implements our translation of DTT into HOL should contact me.  It handles both
"subtypes" and the kind of uses of dependent types Keith Hanna talked about.

I don't have a copy of Keith Hanna's slides that were referred to above, but
concerning the use of dependent types in hardware verification (e.g. for n-bit
words) I recommend the following papers:
   
    F. K. Hanna, N. Daeche, and M. Longley,
    `Specification and Verification Using Dependent Types', 
    IEEE Transactions on Software Engineering,
    vol. 16, no. 9 (September 1990), pp. 949-964.

    M. Leeser,
    `Using Nuprl for the verification and synthesis of hardware',
    in Mechanized Reasoning and Hardware Design,
    edited by C. A. R. Hoare and M. J. C. Gordon,
    Prentice Hall International Series in Computer Science
    (Prentice Hall, 1992), pp. 49-68.

    P. B. Jackson, 
    `Nuprl and its Use in Circuit Design',
    in Theorem Provers in Circuit Design: Theory, Practice and
    Experience: Proceedings of the IFIP WG10.2 International
    Conference, Nijmegen, June 1992, edited by 
    V. Stavridou, T. F. Melham, and R. T. Boute
    (North-Holland, 1992), pp. 311-336.

Tom