Source : Free On-Line Dictionary of Computing

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)