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