In 1998 the University of Manchester published my Computer Science PhD thesis, The Machine-Checked Literate Formalisation of Algebra in Type Theory.
However, they've long since lost the electronic version from their servers, so here are my personal copies.
THE MACHINE-CHECKED
LITERATE FORMALISATION OF
ALGEBRA IN TYPE THEORY
A thesis submitted to the University of Manchester
for the degree of Doctor of Philosophy
in the Faculty of Science and Engineering
January 1998
By
Anthony Bailey
Department of Computer Science
I present a large-scale formalisation within a type theory of a proof of a result from abstract algebra. The formalisation body consists of files that are machine-checked to ensure their correctness, and also processed to produce a report on the proof that is human-readable. The resulting presentation is intended to approach being a standard informal account of some mathematics.
In addition to presenting this proof, the thesis also identifies and examines problems in reconciling the formal nature of the development with the wish for it to be easy to read. It presents some tools and methodologies for solving these problems, and discusses the advantages and disadvantages of these solutions. In particular, it addresses the implementation and use of implicit coercions within the type theory, the styles of proof that can be used, and the borrowing of concepts from the literate programming paradigm.
To be more specific, the algebra in question is a constructive version of the fundamental theorem of Galois Theory. The formalisation is developed within a variant of the Unified Theory of Types that is implemented by a modified version of the LEGO proof-checker.
These versions were reconstructed from a DVI copy festering on the CD of stuff I was able to take away from Manchester. My thanks to Freek Wiedijk for generating them. I believe this is the final version of the thesis, including corrections, apart from some missing title pages that I originally printed separately for some obscure LaTeX page-numbering reason.
I still have the source files for the formalisation and for the thesis. In fact, they are one and the same - it was formally and literally a literate formalisation!) Unfortunately I was not able to take with me a copy of source or binaries for the modified version of LEGO which did the proof-checking and pretty-printing, and these too have long since been deleted from the university servers. If anyone wants said source files, though, they should let me know.
FIXME: are there some Dublin Core metadata attributes I should put into this page? Please let me know if so!