@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@D

Name: Nuprl

Keywords:  intuitionistic, propositions as types, 
    proof by refinement, program extraction

Description: 
   Semantics:  intuitionistic type theory, based on Martin Lof type theory
   Deductive machinery:  proof by refinement in natural deduction calculus
   Dynamics:  notation definitions, ???
   Persistence: library facilities ?? fill in

Contact persons: 
howe@cs.cornell.edu


User group: ?? <user-mailing list, publications>

Pragmatics:  ??  <strengths/weaknesses>

Documentation:  <manuals, tutorials, demos>
R. L. Constable et. al.
Implementing Mathematics with the Nuprl Proof Development System
Prentice Hall
1986

Applications: ??
   <list of major applications -- brief description of problem and result,
   pointer to more info>

Extensions/enhancements:

Resource requirements:

Version 3.1 of the Nuprl Proof Development System is now available. [Aug90]
It now should be possible to run Nuprl on a Symbolics Lisp Machine, 
a Sun running the SunView window system, and any Unix machine running 
X-windows and a commercial Common Lisp with CLX..
We have tested Nuprl 3.1 on the following.
\begin{itemize}
\item Sun 3's, Sun 4's and SPARCstations running Sun (Lucid) Common Lisp
3.0 with the SunView window system and with X-windows and CLX.
\item DECstation 3100's with Lucid 3.0, X-windows and CLX.
\item A Silicon Graphics Iris 4D machine with X-windows, Allegro
Common Lisp 3.1 and CLX.  
\item Symbolics machines (36xx with Genera 7.2
and MacIvory with Genera 7.4I) using the Symbolics window system.
\end{itemize}
Recent versions of Allegro and Lucid may come with their own version of
CLX.  The Nuprl distribution tape also includes a version.  

Where-to-get-it:

To cover our costs, we are charging new recipients of Nuprl \$150 for
the distribution package.  The package includes a tape and the book
{\em Implementing Mathematics with the Nuprl Proof Development
System}.  The tape includes the source code for Nuprl, some of the
Nuprl libraries that have been constructed at Cornell, and some
documentation files that supplement the book.  Those who have paid for
a previous distribution package can obtain a Nuprl 3.1 tape free of
charge.

When requesting a copy of the system, please specify what kind of tape
you would like: a cartridge in Symbolics' ``carry'' format, a tar-format
cartridge, or tar-format reel.  Please make any cheque payable to ``Nuprl
Project''.

Please direct all correspondence to:
Elizabeth Maxwell
Nuprl Distribution Coordinator
Department of Computer Science, Upson Hall
Cornell University
Ithaca, NY 14853. 

[info source, date] 
email announcement 1990

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%