*From the introduction:*

LEGO is an interactive proof development system (proof checker) designed and implemented by R. Pollack in Edinburgh. It implements various related type systems --- the Edinburgh Logical Framework [HHP87], the Calculus of Constructions [CH88], the Generalized Calculus of Constructions [Coq86] and the Extended Calculus of Constructions [Luo89,90]. An overview of the basic theory and implementation of LEGO may be found in [Pol88], where most of the features of the system are sketched and explained, and a simple and informal introduction to the system can be found in [Bur89b]. In Pollack's forthcoming PhD thesis [Pol92], one may find much more detailed development on the system with a lot of interesting examples. As LEGO is still in the process of development, this document only describes the basic features of the current system so that it can be used by more people who are interested in theorem proving and program specification and development.

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, the features of the system like argument synthesis [Pol90, CH88] and universe polymorphism [Pol90, HP91, Hue87] 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 [CH88, Luo89,90], plus the support of specifying new inductive types, provides an expressive language for formalization of mathematical problems and program specification and development. Particularly, the type universes in the type theory make it possible to formalize abstract mathematics, and the strong sum types (Sigma-types) can be used to naturally express abstract structures, mathematical theories [Luo91a, LPT89] and program specifications [Bur89a, BM91, Luo91b, McK92]. LEGO may also be used to formalize different logical systems and prove theorems based on the defined logics (c.f., [HHP87]).

LEGO has been extensively used by many people and a lot of examples in theorem proving and program development have been done using it. These include a proof of the strong normalization theorem of the second-order lambda-calculus [Ber90], the proof of Tarski's fixpoint theorem [Pol92], a formalization of generalized type systems [Pol92], development of the constructive real numbers from the rationals and the completion of a metric space [Jon91], a proof of Chinese Remainder Theorem [McK92], program specifications and program correctness proofs [BM91, Luo91b, Hof91, McK92], development of a type synthesis algorithm for the simply typed lambda-calculus (Pollack), formalizations of notions of sets [Mah91, Col91], a proof of Schroëdre-Bernstein Theorem (Hofmann), a proof of an isomorphism theorem for universal abstract algebra (Fairtlough), specification and implementation of the Odd-Even Transposition Sorter (Fairtlough, in progress), and proofs of the binomial theorem for rings and a bisimulation equivalence [Tay88,89].

Although we do not assume the reader is familiar with type theories, we do not explain basic type-theoretic notions. Instead, we try to give some intuitive analogies to help its understanding. LEGO users interact with the top level of ML [HMM86]. They are not required to be familiar with ML language, although some basic knowledge about ML would be useful. We do not assume that the reader of this manual has knowledge about ML.

Previous | Index | Next