nuprl
     
        /nyu prl/ 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
     
     
see also:
franz lisp edinburgh ml