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)