Main page

Objectives and state of art

Research groups

Software

Tutorials and advanced lectures

The Types mailing list

Previous events

Organisation

Contact

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:

• Correctness of computer systems: We will work on dependently typed programming, among others. Currently, a 3-year project funded by UK EPSRC is in progress to develop the basic technology and a platform for dependently-typed programming. There is a planned workshop on this topic (in year 1) in the current proposal.
• Formal mathematics and mathematics education: We will work on this topic by developing associated proof tools for mathematics, among other things, in the 3-year project Pythagoras, funded by UK EPSRC and joint with the Manchester site of this proposal.
• Proof technology: We will further develop the proof assistant Plastic, studying the implementation techniques and developing its applications (including domain-specific reasoning).
• Foundational research: We will continue to work on logical frameworks, subtyping, and extensionality.

The key members are:

• Zhaohui Luo, contact person
• Conor McBride
• Yong Luo

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