Atomics is a very intricate theorem and can be worked out with

algebra but you would want to take it by degrees because you

might spend the whole night proving a bit of it with rulers

and cosines and similar other instruments and then at the

wind-up not believe what you had proved at all. If that

happened you would have to go back over it till you got a

place where you could believe your own facts and figures as

delineated from Hall and Knight's Algebra and then go on again

from that particular place till you had the whole thing

properly believed and not have bits of it half-believed or a

doubt in your head hurting you like when you lose the stud of

your shirt in bed.Flann O'Brien, The Third Policeman

*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.

*Acknowledgements:* Rather than the usual technical
acknowledgements, I have written a history of LEGO (section 1.2)
and of the project reported in this thesis (section 1.3). In those
sections I try to say who and what were the important influences on
this work. I thank all of them, as I have loved doing the work.

I also want to thank LFCS and the many friends I have here. Rod Burstall, my research supervisor, has endless enthusiasm for computer aided formal reasoning, and has supported and encouraged my work. I especially want to thank George Cleland, who, as administrator of LFCS, has always supported research over red tape. LFCS has always managed to find the resources I asked for.

Talking about resources, this thesis burned more computer cycles
than most, and I don't just mean for *LaTeX*. The computing
services available at LFCS are the best I have encountered. Thanks
to Paul Anderson, George Cleland, Morna Findlay, and many other
CO's.

Finally, I want to thank two people who have influenced my mathematical aesthetic. Gabe Stolzenberg taught me most of what I know about constructive mathematics, and encouraged looking deeply at the meaning of mathematical things. Clint McCrory is a college friend I haven't seen in many years. When I was an undergraduate at M.I.T. and he was a postgraduate at Brandeis, he somehow, through discussion of class problem sets from my second year analysis course, changed me from a mediocre student who enjoyed mathematics, to someone obsessed with the exact shape and presentation of proofs.

This work was supported by the ESPRIT Basic Research Actions on Logical Frameworks (LF) and Types for Proofs and Programs (TYPES), and by grants from the British Science and Engineering Research Council.

This is a 143-page PhD thesis which is available as a 157Kb gzipped DVI file or a 428Kb DVI file or a 212Kb gzipped PostScript file or a 660Kb PostScript file.

Previous | Index | Next