Presently *(uncategorized).

From <em>An Introduction to LEGO</em> (see below):
<blockquote>
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 system)s - the Edinburgh Logical Framework (LF), the Calculus of Constructions (CC), the Generalized Calculus of Constructions (GCC) and the Unified Theory of Dependent _(Type)s (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 _(type)s, provide an expressive language for formalization of mathematical problems and program specification and development.

...
</blockquote>

<ul class="implementations">
<li>_("Lego Homepage"|http://www.dcs.ed.ac.uk/home/lego/).
</ul>

<ul class="links">
<li>_("An Introduction to LEGO"|http://www.dcs.ed.ac.uk/home/lego/html/intro.html).
</ul>
