Nuprl
A system for manipulating proofs based on the type theory of Martin-Löf. It has been superseded by the Formal Digital Library. See also the page for the PRL project.

Application Mathematics Theorem Provers