Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Tue, 13 Jun 1995 05:18:26 +0100
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA076245633;
          Mon, 12 Jun 1995 21:53:53 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Received: from aohakobe.ipc.chiba-u.ac.jp by leopard.cs.byu.edu 
          with ESMTP (1.37.109.15/16.2) id AA076215631;
          Mon, 12 Jun 1995 21:53:51 -0600
Received: from aohakobe (localhost [127.0.0.1]) 
          by aohakobe.ipc.chiba-u.ac.jp (8.6.12/3.4Wbeta3 (-: 95041617) 
          with ESMTP id MAA18412; Tue, 13 Jun 1995 12:54:43 +0900
Message-Id: <199506130354.MAA18412@aohakobe.ipc.chiba-u.ac.jp>
To: Wishnu Prasetya <wishnu@cs.ruu.nl>
Cc: info-hol@leopard.cs.byu.edu
Subject: Re: reference to nuperl
In-Reply-To: Your message of "Mon, 12 Jun 1995 20:20:53 +0200." <Pine.HPP.3.91.950612201931.12399K-100000@muddy.cs.ruu.nl>
Date: Tue, 13 Jun 1995 12:54:42 +0900
From: Yozo Toda (TELEPHONE +81-43-290-3539) <yozo@aohakobe.ipc.chiba-u.ac.jp>


> Can someone help me with references to some good introduction book to
> nuperl?

I found the WWW home page of Nuprl
	<http://www.cs.cornell.edu/Info/Projects/NuPrl/index.html>
        Cornell Nuprl Automated Reasoning Project

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

Honestly, I haven't seen Nuprl working on real machines...

-- yozo.