Early in the 20th century, mathematics has seen a strong move towards abstraction, in particular in the field of algebra. Many branches of mathematics benefited from re-useable knowledge that could be applied easily.

The same is desirable when working with interactive provers. Today, formalisations of algebra in provers are normally geared towards particular applications, and their reuse is restricted. We work towards a comprehensive library of basic algebra, which can be flexibly reused. The development of the library is an ongoing project. It currently provides groups, rings and polynomials. The library in its current state (http://isabelle.in.tum.de/dist/library/HOL/HOL-Algebra/index.html) is available with the distribution of Isabelle and is based upon its main logic HOL.

The library is used in the verification of the computer algebra systems Kenzo (http://www-fourier.ujf-grenoble.fr/~sergerar/Kenzo/), which is a specialised system for computations in Homological Algebra.

For all matters related to this topic, please contact Clemens Ballarin.

Isabelle (http://isabelle.in.tum.de) is a generic interactive theorem prover developed by Lawrence C. Paulson at the University of Cambridge and Tobias Nipkow at TU München. Isabelle is being used for a range of verification applications, and also for formalisations in various branches of mathematics (see the Isabelle projects page: http://isabelle.in.tum.de/projects.html).

Our research in Innsbruck is centered around Isabelle. It is concerned with the module system of Isabelle, the formalisation of abstract algebra and with applications thereof.

Most modern programming languages provide modules or classes to break up code into chunks convenient for humans, and to enable effective reuse. Modules for provers correspond to mathematical theories and are less common. They are essential, though, if large systems are to be verified.

The requirements of modules in provers are more complex than in programming languages: not only can relations between modules be declared (through import or inheritance), they may also be derived. Secondly, modules may be extended after their declaration. Finally, reuse should be possible in all kinds of contexts, including in proofs.

Locales are the theory development modules of Isabelle. While an increasing number of provers can handle derived relations between modules (theory interpretation), it is normally not possible to reopen modules in order to add theorems that were not provided by the module developer, say. We achieve this by explicitly maintaining module dependencies in a development graph. Locales are integrated with Isar, Isabelle’s language for readable proof documents, and we provide interpretation of locales in the context of proofs.

Abstract algebra constitutes an excellent testbed for a module system. Locales are also applied in other domains — for example, in software verification.

Modern engineering applications have reached a level of complexity where the judgement of experts is no longer sufficient to ensure their correctness. This is true, in particular, for software systems. Theorem provers can, in principle, be used to rigourously check the correctness of such systems. This is achieved in a two-step process: first, the desired properties (the specification) of the software are described in a formal mathematical language; then, a formal proof is constructed to show that the implementation of the software meets these properties. The latter is called verification or certification. Since the proof is machine-checked gaps and mistakes, which are frequent in informal arguments, can be avoided.