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)
Nearby terms:
numbers « number sign « Numeris « Nuprl »
NU-Prolog » nurbs » Nu Thena
|
