# 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:

## 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.

## People

*(alphabetical order)*
## Other Links

Markus Wenzel 13-Oct-1997