Report on the Tatami System

by Rod Burstall
Professor Emeritus of Computer Science, Edinburgh
December 2000

It is clear that the creation of systematic bodies of mathematical knowledge on computing systems requires the cooperation of a large number of researchers. Let us call such a body including definitions, theorems and proofs a "theory"; the components of a theory may be formal or partly informal and the subject matter may be purely mathematical or refer to some area of computing such as a programming language or a collection of related algorithms. A number of projects have tried to build up theories as a "library" for a particular prover, and the Mizar project originating in Poland has collected machine checked proofs from a considerable number of contributors. The Tatami project aims to take this a step further by allowing theories to be built up using the World Wide Web. It has to address several problems, as follows:

Here are some comments on how Tatami tackles the above problems: These facilities provide an innovative approach to distributed theory production. The potential of the system is much greater than the present system given the possibility of incorporating other proof tools. The Duck language and its ability to generate web pages with readable proofs is especially interesting, and the use of XML for transferring data between proof systems without having to write parsers should be further explored. Altogether the user interface encourages the user to work through the examples and using the links to dig more deeply into aspects of the system which interest her.

An impressive aspect of Tatami, not discussed above is the BOBJ proof system for behavioural equivalence. It includes an efficient and easy to use algorithm for coinduction, with a more general version of coinduction available through Duck. The behavioral equivalence and hidden algebra features enable one to handle infinite data types such as streams in a natural way, as well as treating objects as in object oriented programming. The induction facilities of OBJ are also available. The system is small and efficient.

In summary, Tatami is an attractive, well designed and well implemented system, making excellent use of the world wide web and the Java programming language. It has a number of ideas which are substantial contributions to the state of the art, and it is unusual in the pains taken to make it accessible over the web to anyone concerned with cooperative development of mathematical theories.

To the Tatami project homepage
To the research projects homepage
Maintained by Joseph Goguen Last modified: Wed Jan 3 16:32:28 PDT 2001