PRL
The Proof (or Program) Refinement Logic program, led by Robert Constable of Cornell. Systems from the project include Nuprl and the Formal Digital Library.

Mathematics