- Foundational research includes work on inductive and coinductive definitions, especially induction-recursion, on proof theoretically strong extensions of type theory, and on totality and termination.
- Work on correctness of computer systems includes programming with dependent types (especially interactive programs), object-oriented programming in type theory, and extraction of programs from classical proofs.
- Work on proof technology will be case studies applying interactive theorem proving to algebraic specification languages.

- Ulrich Berger (reader)
- Andy Gimblett (tutor)
- Markus Michelbrink (senior research assistant)
- Markus Roggenbach (lecturer)
- Monika Seisenberger (tutor)
- Anton Setzer (lecturer; contact person)

Anton Setzer Last modified: Mon Oct 3 21:53:52 BST 2005