catflap.org Online Dictionary Query |
From The Free On-line Dictionary of Computing (27 SEP 03) : [ foldoc ]
Nuprl
/nyu p*rl/ Nearly Ultimate PRL.
A system for interactive creation of formal mathematics,
including definitions and proofs. It has an extremely rich
type system, including dependent functions, products, sets,
quotients and universes. Types are first-class citizens.
It is built on Franz Lisp and Edinburgh ML.
["Implementing Mathematics in the Nuprl Proof Development
System", R.L. Constable et al, P-H 1986].
(1994-12-13)