Next: LEGO projects
Up: Contents
Previous: Contents
An Introduction to LEGO
LEGO is an interactive proof development system (proof assistant)
designed and implemented by
Randy Pollack in Edinburgh using New Jersey ML. 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).
LEGO is a powerful tool for interactive proof development in the
natural deduction style. It supports refinement proof as a basic
operation. The system design emphasizes removing the more tedious
aspects of interactive proofs. For example, features of the system
like argument synthesis and universe polymorphism make proof checking
more practical by bringing the level of formalization closer to that
of informal mathematics. The higher-order power of its underlying type
theories, and the support of specifying new inductive types, provide
an expressive language for formalization of mathematical problems and
program specification and development.
Particularly, Zhaohui Luo's
type theory UTT includes:
- type universes, which make it possible to formalize abstract
mathematics;
- strong sum types, which can be used to naturally express
abstract structures, mathematical theories and program specifications,
and
- a schema for inductive data types, which captures the common inductive
structures in programming languages and mathematics.
LEGO may also be used to formalize different logical systems and prove
theorems based on the defined logics, following the philosophy of the
Edinburgh Logical Framework.
For further information, go to the Contents page.