Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Date: Tue, 13 Jun 95 10:28:52 EDT
From: mel@ultrastar.EE.CORNELL.EDU (Miriam Leeser)
Message-Id: <9506131428.AA12042@ultrastar.EE.CORNELL.EDU>
To: yozo@aohakobe.ipc.chiba-u.ac.jp
Cc: wishnu@cs.ruu.nl, info-hol@leopard.cs.byu.edu
In-Reply-To: Yozo Toda (TELEPHONE +81-43-290-3539)'s message of Tue, 13 Jun 1995 12:54:42 +0900 <199506130354.MAA18412@aohakobe.ipc.chiba-u.ac.jp>
Subject: reference to nuprl


Nuprl works on probably all the architectures that HOL works on.  The
new system Nuprl 4 is written in an old version of ML (apparently even
older than that used for HOL88) that runs on top of LISP.  I use a
sparc startion to run Nuprl 4.  Nuprl 5, currently under development
is written in SML, much like HOL90.  Nuprl 3 also runs on unix
boxes running  lisp.  I don't know what you mean by a real machine.

I have done extensive work on hardware verification in Nuprl.  
References to my work and how to get some relevant papers are listed
below.  Others at Cornell are using Nuprl for algebra, distributed
systems verification and other applications.

Nuprl is used at several other sites as well as at Cornell.  There is
a nuprl mailing list: nuprl-notes@cs.cornell.edu

The best source for information about nuprl is indeed the web-site at
Cornell:
  <http://www.cs.cornell.edu/Info/Projects/NuPrl/index.html>

The web site includes information about the system, documentation, etc.

The book: 
  
	"Implementing Mathematics with the Nuprl Proof Development System",
	R.L.Constable et al., Prentice-Hall, 1986.


The book is still the best source of information about the logic, but
the system has changed quite a bit in the ten years since the book
was written.  In particular the book describes the Symbolics version
of the system.  When the book was written there was already a unix version.

And the system is called Nuprl, for Nu Programming Refinement Logic

Some of my relevant papers are available from 

  ftp://tesla.ee.cornell.edu/ftp/pub/hw-verify

Papers you might be interested in are:

@inproceedings{leeser-rsoc92,
	author = {Miriam E. Leeser},
	title = {Using {Nuprl} for the Verification and Synthesis of Hardware},
	booktitle = {Mechanized Reasoning and Hardware Design},
	year = {1992},
	publisher = {Prentice-Hall International Series on Computer Science},
	editor = {C. A. R. Hoare and M. J. C. Gordon}
}

@inproceedings{aagaard-hol93,
 author    = {Aagaard, Mark D. and Leeser, Miriam E. and Windley, Phillip J.},
 title     = {Towards a Super Duper Hardware Tactic},
 booktitle = {HOL Theorem Proving System and its Applications},
 year      = 1993,
 month     = {August},
 publisher = springer-verlag,
 editor    = {Jeffrey J. Joyce and Carl-Johan H. Seger},
}

@inproceedings{aagaard-hol92,
        author  = {M. Aagaard and M. Leeser},
        title   = {A Methodology for Reusable Hardware Proofs},
        booktitle = {HOL Theorem Proving System and its Applications},
        year    = {1992},
        month   = {September},
        publisher = {North-Holland},
        editor  = {Luc Claesen and Mike Gordon}
}

A longer version of this paper was published in the Formal Methods and
System Design journal published by Kluwer, July, 1994.