The LEGO Proof Assistant
Library Home || Full Table of Contents || Library Help
|Randy Pollack; University of Edinburgh|
|A tool for interactive proof development in the natural deduction style. It implements various related type systems - the Edinburgh Logical Framework (LF), the Calculus of Constructions (CC), the Generalized Calculus of Constructions (GCC), and the Unified Theory of Dependent Types (UTT). It supports refinement proof as a basic operation. The system design emphasizes removing the more tedious aspects of interactive proofs.|
|Resource Types:||Topic Tools Miscellaneous|
|Math Topics:||Logic/Foundations, Computer Science|
© 1994- The Math Forum at NCTM. All rights reserved.