Up: Cooperating sites
The Swansea subsite, at the Dept. of Computer Science, University of Wales, is particularly strong in mathematical logic and foundations of type theory, but also has interests in applications to programming languages. The site plans to contribute to three of the objective areas.
- 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.
The senior members of the Swansea subsite are:
- Anton Setzer (contact person)
- Ulrich Berger
- Markus Roggenbach
Bengt Nordström 2005-09-22