The Swansea subsite of the TYPES Project
The Swansea subsite, at the
University of Wales Swansea,
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
The members of the Swansea subsite are:
- 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.
Last modified: Mon Oct 3 21:53:52 BST 2005