Formal Digital Library

A product of the PRL project and descendant of the Nuprl system, FDL is a system implemented in Common Lisp for developing, refining, and collecting formal proofs. It is based on the constructive type theory of Martin-Löf.

Application Mathematics Theorem Provers

This page is linked from: Nuprl PRL

CLiki pages can be edited by anyone at any time. Imagine a fearsomely comprehensive disclaimer of liability. Now fear, comprehensively