The "Deduktion" Project in München

Verification in Higher Order Logic is the focus of our Deduktion group. We have done work in the areas of functional programming, equational reasoning, and distributed systems, developing working systems, theoretical investigations, and case studies. Currently, we are working on deductive systems for OO programming languages. We develop and use in our work the generic theorem proving environment Isabelle, especially the Isabelle/HOL instantiation.

Functional Programming

Our work on functional programming comprises a mechanization of LCF, a well-known logic for computable partial functions, and a mechanization of total functions. These systems inherit all of the theory and proof infrastructure of Isabelle/HOL and are therefore suitable for large-scale proof efforts.

System: HOLCF -- Domain Theory in Higher Order Logic (implementation).
System: TFL -- Total functions (see also TFL page).

Equational Reasoning

We have investigated higher-order equational reasoning and lifted several methods and results from the first-order to the higher-order context. We have shown that this can be applied to get a functional programming language that gracefully accommodates some logic programming concepts. Selected references:

R. Mayr, T. Nipkow. Higher-Order Rewrite Systems and their Confluence. Theoretical Computer Science, to appear.
C. Prehofer, Higher-order Narrowing. In Proceedings, Ninth Annual IEEE Symposium on Logic in Computer Science, 1994.
C. Prehofer, Solving Higher-Order Equations: From Logic to Programming (PhD. Dissertation).
C. Prehofer, Higher-Order Narrowing with Convergent Systems, Proceedings, AMAST 1995.

Distributed Systems

In this area, we have mainly focused on developing a mechanization of the meta-theory of Nancy Lynch's theory of I/O automata. Several protocols have been verified on top of this foundation. Also, we have started to investigate ways of combining automatic tools with our interactive theorem proving approach.

The Seven Author Protocol (paper, implementation).
Combining model checking and deduction for I/O automata (paper, implementation).
Formalization of I/O automata in Isabelle/HOLCF (paper).

Case Studies

We have analyzed, proposed, and developed facilities for interactive proof systems. Also, we have performed various significant verifications.

Interactive proof system suggestions (paper).
Proof Management (paper).
A simple while-language, various semantics for it, and their relationships (paper, implementation).
Interpreter Verification for a Functional Language (paper).
Algorithm W for ML type inference - the monomorphic case (paper, implementation).
WAM Verification (paper, implementation).
Church-Rosser theorems for beta and eta reduction in untyped lambda-calculus (paper, implementation).
Algorithm W for ML type inference (paper, slides and implementation).

OO Programming Languages

We are currently working on DOPS (Deduction for OO Programming). In particular on formalization of the type system and the semantics of a substantial subset of Java. See the Bali page for more information.

People

(alphabetical order)