Next: Nijmegen
Up: Cooperating sites
Previous: LMU München


TU Munich

The group at TU Munich, which has participated in the last two TYPES projects, is focused on the development of both further improvement of the theorem prover Isabelle, and on its applications. On the improvement side, our group has developed the Isar environment for writing human-readable proof documents, as well as a module system called Locales, which allows for a more elegant and scalable presentation of mathematical theories. This work led to a joint journal paper with the Nijmegen group comparing the Isar and Mizar systems.

Moreover, thanks to a recently developed extension of its kernel, Isabelle can now generate primitive proofs, represented as -terms in the spirit of the Curry-Howard isomorphism. This allows for an independent verification of proofs produced by Isabelle and forms the basis for future applications such as proof-carrying code, or the exchange of proofs with other theorem proving systems. Based on this representation of proofs, we have introduced a new generic framework for the extraction of programs from constructive proofs conducted in Isabelle. This has been carried out in cooperation with the group of Prof. Schwichtenberg from the LMU Munich site.

On the applications side, emphasis was on programming language semantics, and formalised mathematics. We have continued our work on formalising programming languages and treated substantial parts of the Java language, such as operational semantics for both the source and bytecode level, a compiler from source code to bytecode, as well as Hoare logics. We are in the process of obtaining the first bytecode verifier for the Java Virtual Machine that has a machine-checked correctness proof, covering even advanced features such as bytecode subroutines and object initialization. Moreover, we are currently evaluating both the concept and the implementation of Locales by applying it to a formalisation of abstract algebra. An Algebraic Base Library for Isabelle, of which a first version was released with Isabelle 2003, is being developed jointly with L. Paulson (University of Cambridge), and H. Kobayashi (Nihon University). The developed algebraic library will be used to prove results in algorithmic algebraic topology, which is a first step to increase the reliability of symbolic computation systems in this area.

Future research will mainly focus on the objective of Correctness of Systems:

Integrated environment for proving and programming

A long term goal is to achieve a tighter integration of specification, proving, programming and testing. To this end, we have already extended Isabelle with a mechanism for generating executable code from specifications, which covers inductive datatypes, inductive predicates and recursive functions. Based on this code generator, we are currently developing a framework for testing specifications by evaluating logical formulae with respect to a mapping of free variables to random values. This project is inspired by the QuickCheck tool developed at the Chalmers site, which was originally designed for testing Haskell programs, and has now also been integrated into the Agda / Alfa proof editor.

Proof-carrying code

We are currently developing a formally verified framework for proof-carrying code. A particular application of this framework is the certification of resource bounds (i.e. for time and space) of programs. In this respect, we will closely collaborate with research groups at LMU München (Prof. Martin Hofmann) and Edinburgh (Dr. David Aspinall).

The senior members involved in the TYPES project are:

TU Munich homepage

Bengt Nordström 2005-09-22