The Nuprl system, based on the type theory of Martin-Löf, is a system for manipulating proofs. By default Nuprl runs in the cloud, and is intended primarily to be used as a web service rather than as standalone software. Nuprl is a product of the PRL project.
Application Mathematics Theorem Provers
Nuprl