NuPrl Proof Development System
Library Home || Full Table of Contents || Library Help
|Cornell University, Ithaca, NY|
|A tactic-based proof assistant developed over the last 15 years at Cornell University. Its features include: very expressive logical language based on Martin-Lof type theory, extensive library of formal mathematics and automata theory, possibility of an extraction a certified program from the constructive proof of its formal specification, graphical proof editor. NuPrl was successfully used in verifying components of the Ensemble group communications system.|
|Resource Types:||Topic Tools Miscellaneous|
|Math Topics:||Logic/Foundations, Computer Science|
© 1994- The Math Forum at NCTM. All rights reserved.