This project explores the logical and type theoretical foundations of
formal mathematical proof and its application in computing. The
following aspects characterize our approach:
- The development of logical formalisms that support natural
and compact descriptions of mathematics and computer science.
- The implementation of interactive theorem provers for the
above formalisms. We aim to support the rapid construction of
mechanizations, along with a high-level style of interactive proof.
- The application of our theories and tools to concrete problems in
computing; for example, in the verification of programs, protocols
and hardware.
The focus of our work is the generic theorem prover Isabelle,
which was developed at Cambridge University. Isabelle is generic in
the sense that it can be instantiated with the syntax and inference
rules of a logic. Isabelle is constantly being enhanced in a close
collaboration between Cambridge and Munich. Another
branch of our work is large case studies: for example, we have done
verifications of Milner's type inference algorithm W, programming language
semantics, protocols, and lambda calculus theory. Moreover, we have
developed libraries for abstract algebra and graph theory. Further
work is in progress even now while you are surfing the net!
Check out Isabelle's
main page.
People
For a list of researchers involved in the project, see the homepage of the
theorem proving group.
Subsite:
Universität Bamberg
Representative:
Michael Mendler
Stefan Berghofer
Last modified: Wed Oct 27 15:54:53 MEST 2004
