The Free On-line Dictionary of Computing (30 December 2018):

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)