You are here: irt.org | 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)
Nearby terms: number sign « numeric keypad « Numeris « Nuprl » NU-Prolog » nurbs » Nu Thena
FOLDOC, Topics, A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, ?, ALL