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