Nuprl(ID:1244/nup001)

(pronounced "new pearl") Nearly Ultimate PRL. Interactive creation of formal mathematics, including definitions and proofs. An extremely rich type system, including dependent functions, products, sets, quotients and universes. Types are first-class citizens. Built on Franz Lisp and Edinburgh ML.
Related languages
Edinburgh ML => Nuprl   Based on
FranzLISP => Nuprl   Based on
PRL => Nuprl   Evolution of
References:
  • Constable, R.L. et al, "Implementing Mathematics in the Nuprl Proof Development System", P-H 1986. view details