Theory of LEGO
dc.contributor.advisor
Burstall, Rod
en
dc.contributor.author
Pollack, Robert
en
dc.contributor.sponsor
ESPRIT Basic Research Actions on Logical Frameworks (LF) and Types for Proofs and Programs (TYPES)
en
dc.contributor.sponsor
British Science and Engineering Research Council
en
dc.date.accessioned
2004-06-15T08:54:56Z
dc.date.available
2004-06-15T08:54:56Z
dc.date.issued
1995-07
dc.description.abstract
LEGO is a computer program for interactive typechecking in the Extended Calculus of Constructions and two of its subsystems. LEGO also supports the extension of these three systems with inductive types. These type systems can be viewed as logics, and as meta languages for expressing logics, and LEGO is intended to be used for interactively constructing proofs in mathematical theories presented in these logics. I have developed LEGO over six years, starting from an implementation of the Calculus of Constructions by Gérard Huet. LEGO has been used for problems at the limits of our abilities to do formal mathematics.
In this thesis I explain some aspects of the meta-theory of LEGO's type systems leading to a machine-checked proof that typechecking is decidable for all three type theories supported by LEGO, and to a verified algorithm for deciding their typing judgements, assuming only that they are normalizing. In order to do this, the theory of Pure Type Systems (PTS) is extended and formalized in LEGO. This extended example of a formally developed body of mathematics is described, both for its main theorems, and as a case study in formal mathematics. In many examples, I compare formal definitions and theorems with their informal counterparts, and with various alternative approaches, to study the meaning and use of mathematical language, and suggest clarifications in the informal usage.
Having outlined a formal development far too large to be surveyed in detail by a human reader, I close with some thoughts on how the human mathematician's state of understanding and belief might be affected by possessing such a thing.
en
dc.format.extent
821811 bytes
en
dc.format.extent
659953 bytes
en
dc.format.extent
427788 bytes
en
dc.format.mimetype
application/pdf
en
dc.format.mimetype
application/postscript
en
dc.format.mimetype
application/x-latex
en
dc.identifier.uri
http://hdl.handle.net/1842/504
dc.language.iso
en
dc.publisher
University of Edinburgh. College of Science and Engineering. School of Informatics.
en
dc.subject.other
LEGO
en
dc.subject.other
type system
en
dc.title
Theory of LEGO
en
dc.title.alternative
The Theory of LEGO
dc.type
Thesis or Dissertation
en
dc.type.qualificationlevel
Doctoral
en
dc.type.qualificationname
PhD Doctor of Philosophy
en
Files
This item appears in the following Collection(s)