NUPRL

("new pearl") Nearly Ultimate PRL

A language for the interactive creation of formal mathematics, including definitions and proofs. It features an extremely rich type system, including dependent functions, products, sets, quotients and universes. Types are first-class citizens. Implemented in Franz Lisp and LCF ML.

"Implementing Mathematics with the Nuprl Proof Development System", R. L. Constable et al, Prentice-Hall, 1986.