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
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).
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:
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.
We have analyzed, proposed, and developed facilities for interactive
proof systems. Also, we have performed various significant
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.
Markus Wenzel 13-Oct-1997