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)