LEGO Algebra Group

Welcome to the (probably misleadingly named) LEGO Algebra Group homepage.

Contents of this page

Outline of the LAG project

Here is some text from Peter Aczel that outlines the purposes of this Group:

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. Peter Aczel, Henk Barendreght, Gilles Barthe and Zhaohui Luo. I would also like to include Anthony Bailey.

We share a common interest in the use of LEGO and perhaps similar systems such as Coq and Alf 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.

  1. 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 Manchester)
  2. 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.
  3. 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.
  4. 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 and plans.

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

The references I have so far fall into several sections.

Coercions, classes and sub-typing

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 synthesis, or 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.
Work on coercive subtyping within type-theories
Subtyping using record types
This involves the incremental definition of subtypes of previous types.
Subtyping using refinement (or intersection) types

Theory and associated mechanisms

The GALOIS project

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.

Other large-scale formalisation case-studies

Literate formalisation

It is important to us that formalisations are easy to read. There already exist a very simple bundle of scripts called LaTeXLEGO 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.

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.