Next: Savoie
Up: Cooperating sites
Previous: CNRS / Paris 7

Royal Holloway

The Department of Computer Science at Royal Holloway, University of London has substantial expertise in type theory and its applications to theorem proving and programming. The group was in the University of Durham and was the co-ordinating site of the previous TYPES consortium. In the last several years, it has made contributions to TYPES-related research topics, including development of logical frameworks and type theories, development and implementation of coercive subtyping, implementation of proof assistants, development of proof technology, and design of a platform for dependently-typed programming.

The activities will contribute to the objectives of the proposal:

The key members are:

The work of the group is currently supported by two UK EPSRC grants, as well as the EU TYPES grant. It has close collaborations with several TYPES sites and has had fruitful visits from and to other TYPES sites, including Manchester, Paris Sud, Nottingham, and Edinburgh. These collaborations and visits have greatly advanced the research activities; the TYPES consortium provides an excellent platform for the research activities in this area.

Royal Holloway homepage

Bengt Nordström 2005-09-22