LEGO Algebra Group
Welcome to the (probably misleadingly named) LEGO Algebra Group
Contents of this page
Here is some text from Peter Aczel that outlines the purposes of this
The LEGO Algebra Group, or LAG, is my provisional title to refer to
the group of us that met in Utrecht at
CSL96 this autumn; i.e.
Gilles Barthe and
I would also like to include
We share a common interest in the use of
and perhaps similar systems such as
that implement dependent type theories. We are
interested in the development of machine checked abstract mathematics,
particularly algebra. A key issue for us is how informal abstract
mathematics should be represented in a dependent type theory. Another key
concern is to make efforts to close the gap between informal mathematics and
our formalisations as much as possible.
The reason for our meeting at CSL96 was our desire to give the above
shared interests a focus. Here were some plans that were considered.
Set up a web page with a bibliography and url's for reports MSc, PhD
theses, etc that are available. (Anthony Bailey is willing to do this at
Initiate e-mail discussion to set the limits of what we want to focus
attention on. My description, above, of our common interests, is only meant
to be a start.
Work towards the creation of an electronic book to advertise our subject
and already available published and unpublished work. This would probably
involve the need to write abbreviated versions of material unlikely to be
published in the usual way and chapters to create a coherent presentation.
This electronic book could just be made available via our web page. But if
we feel it is worthwhile we could consider a more formal publication,
perhaps as a real book.
Organise a workshop, say for the autumn of 97, possibly as part of the
Types WG, possibly supported by the British MathFit.
I am sure that there are many things that we discussed not yet included
here, but I hope that this is a start in getting formulated our common aims
I suggest that, while Anthony sets up a web home page, we should send him
what we each consider directly relevent references and url's. Also please
communicate any comments and additions, so that we can achieve a good starting
statement of our aims. There is probably a lot more detail I could add, but
I prefer to get us all moving first. Of course a good title/acronym might
be useful (not LAG).
This page is currently a fairly scratchy index of some of the
electronically available resources that might be relevant. If you have
some to add, then please send
them to me. HTML source for a list of links is the best possible
format so that I can just paste it into this page, but any other
format, including an URL to a list of your own, is a quite acceptable
The references I have so far fall into several sections.
- LEGO with implicit coercions
- Anthony Bailey has hacked at the LEGO source to allow the
application of some declared coercions to
be left implicit in the input and output of LEGO expressions in a
manner analagous to the way in which synthesisable arguments to
functions can be left implicit.
There are two implementations. LEGO with coercions, or
legowc, is the first. Some of you may have already worked
with it. The second is a re-implementation, LEGO with coercion
legowcs. This is much improved, and is
based on modifications to the forth-coming beta-version of LEGO, on
which work is still in progress. In
time, all the changes, including the coercion synthesis ones, will be
released as an official Alpha; in the mean time if you are keen then
try the version here.
- Coq with implicit coercions
- The latest version of Coq implements a similar coercion synthesis
system, but takes a different approach to resolving competing paths
through the graph of coercions.
- copy of Typing algorithms in type theory with
We propose and study a new typing algorithm for dependent type
theory. This new algorithm typechecks more terms by using inheritance
between classes. This inheritance mechanism turns out to be powerful:
it supports multiple inheritance, classes with parameters and uses new
abstract classes of functions and sorts. We also define classes as
records, particularly suitable for the formal development of
mathematical theories. This mechanism, implemented in the proof
checker Coq, can be adapted to all typed lambda-calculus.
- Work on coercive subtyping within type-theories
- DVI copy of Coercive subtyping in type theory (Luo).
We propose and study coercive subtyping, a formal
extension with subtyping of dependent type theories such as
Martin-Lof's type theory and the type theory UTT. In this approach,
subtyping with specified implicit coercions is treated as a feature at
the level of the logical framework; in particular, subsumption and
coercion are combined in such a way that the meaning of an object
being in a supertype is given by coercive definition
rules for the definitional equality. It is shown that this
provides a conceptually simple and uniform framework to understand
subtyping and coercion relations in type theories with sophisticated
type structures such as inductive types and universes.
- compressed copy of Implicit coercions in type systems
We propose a notion of pure type system with implicit coercions. In
our framework, judgements are extended with a context of coercions and
the application rule is modified so as to allow coercions to be left
implicit. The setting supports multiple inheritance and can be applied
to all type theories with pi-types. One originality of our work is to
propose a computational interpretation for implicit coercions. In this
paper, we demonstrate how this interpretation allows a strict control
on the logical properties of pure type systems with implicit
- Subtyping using record types
- This involves the incremental definition of subtypes of previous
- Subtyping using refinement (or intersection) types
- gzipped copy of Refinement types for logical frameworks
We propose a refinement of the type theory underlying the LF framework
by a form of subtypes and intersection types. This refinement
preserves desirable features of LF, such as decidability of
type-checking, and at the same time considerably simplifies the
representations of many deductive systems. A subtheory can be applied
directly to hereditary Harrop formulas which form the basis of
lambda-Prolog and Isabelle.
- gzipped copy of Subtyping dependent types
The need for subtyping in type-systems with dependent types has been
realized for some years. But it is hard to prove that systems
combining the two features have fundamental properties such as subject
reduction. Here we investigate a subtyping extension of the system
lambda-P, which is an abstract version of the Edinburgh logical
framework LF. By using an equivalent formulation, we establish some
important properties of the new system, including subject
reduction. Our analysis culminates in a complete and terminating
algorithm which establishes the decidability of type-checking.
More URLs and references are desired!
This was started by Peter Aczel in 1992(?). It is a long-term and
ambitious project to formalise some abstract algebra in a predicative
style, probably within LEGO. The result chosen as a case-study is the
fundamental theorem of Galois theory.
- DVI copy of A Higher-Order Calculus and Theory
We present a higher-order calculus ECC which naturally combines
Coquand-Huet's calculus of constructions and Martin-Lof's type theory
with universes. ECC is very expressive, both for structured abstract
reasoning and for program specification and construction. In
particular, the strong sum types together with the type universes
provide a useful module mechanism for abstract description of
mathematical theories and adequate formalisation of abstract
mathematics... theory abstraction in ECC is discussed as a pragmatic
- gzipped DVI copy of Galois: A Theory Development Project
A report of work in progress, for the Turin meeting on the
Representation of Mathematics in logical frameworks, January 20-23,
- gzipped DVI copy of Notes towards a formalisation of constructive Galois
We give a presentation of constructive Galois theory. This is
intended, when completed, as a pre-formal blueprint for a machine
checked formalisation and forms part of GALOIS, a long term experiment
at an ambitious effort to formalise a significant body of abstract
- Anthony Bailey's Edinburgh MSc project involved LEGO work on
polynomial rings. Unfortunately, I don't actually have an electronic
copy at present - how daft is that? Oh well.
- And my PhD should involve a large bit of the LEGO formalisation of
GALOIS, but, er, it isn't written yet.
- Alex Jones' Manchester MSc project involved LEGO work on finite
As part of the ongoing project to produce a machine
checked development of Galois Theory, this document describes one
way that a portion of linear algebra leading up to the decidable
dependency theorem can be checked by the LEGO proof checker.
It is important to us that formalisations are easy to read. There
already exist a very simple bundle of scripts called
which allow the addition of LaTeX commentary to LEGO source files in
such a way as to allow LaTeX documentation to be extracted; follow the
above link for more details.
- Mark Ruys has developed a large LEGO
Many mathematical notions are formalized like a
prime generator, the concept of universal algebra's,
polynomials rings and the field of complex numbers.
Also a lot of proofs are given, for example of the fact that for every
complex number there exist a k-th root.
Summaries of the LEGO files can be viewed on-line. The whole
library is available by anonymous ftp.
It is possible to imagine more serious attempts at literate
formalisation, which can be seen as applying the idiom of
literate programming to computer-checked formalisations. Link
ideas are welcome, as are implementations!
One now-completed project of interest is the proof-checker
Deva, which had a
DevaWEB assistant that produced such literate formalisations.
- The DevaWEB System: Introduction, Tutorial, User
Manual, and Implementation (Biersack/Raschke/Simons).
We focus on the literate and structured presentation of formal
developments. We present an approach that is influenced by ideas from
Leslie Lamport on how to write proofs, by Donald Knuth's paradigm of
literate programming, and by the ideas of the "Dutch school" on formal
reasoning. We demonstrate this approach by presenting the proofs of
two mathematical theorems - the Knaster-Tarski fixpoint theorem and
the Schroder-Bernstein theorem - formalized in Deva. We discuss to
what degree our aims have been achieved and what is left to be done.
Martin Simon's thesis The presentation of formal proofs
In this thesis we present an approach to the intelligible
communication of formal proofs. Observing a close correspondence
between the activities of formal-proof development and program
development, and using this as a guideline, we apply well-known
principles from program design to proof design and presentation,
resulting in formal proofs presented in a literate style, are
hierarchically structured, and emphasize calculation...
Proof Style (John Harrison)
We are concerned with how to communicate a mathematical proof
to a computer theorem prover. This can be done in many ways, while
allowing the machine to generate a completely formal proof object. The
most obvious choice is the amount of guidance required from the user,
or from the machine perspective, the degree of automation
provided. But another important consideration, which we consider
particularly significant, is the bias towards a `procedural' or
`declarative' proof style. We will explore this choice in depth, and
discuss the strengths and weaknesses of declarative and procedural
styles for proofs in pure mathematics and for verification
applications. We conclude with a brief summary of our own experiments
in trying to combine both approaches.
The Mizar project's Journal Of Formalised
The Mizar project started about 1973 with an attempt to
reconstruct mathematical vernacular. Since 1989, the most important
activity in the Mizar project is development of data base for
mathematics... Journal of Formalized Mathematics is an electronic
counterpart of Formalized Mathematics.
The Journal presents many Mizar proof-scripts which have been designed
to be "readable."