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.

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:

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.

Case Studies

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

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.


(alphabetical order)

Other Links

Markus Wenzel 13-Oct-1997