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].
| < Previous Terms | Terms Containing Nuprl | Next Terms > |
| NUMA number crunching numbers number sign Numeris | Nuprl University of Edinburgh | NU-Prolog nurbs Nu Thena NUXI problem NVRAM |
