/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)