One-Day Workshop on Dependent Type Theory
Wednesday July 19th, 2006

Department of Computer Science
Royal Holloway, University of London


Zhaohui Luo, Royal Holloway, University of London
Robin Adams, Royal Holloway, University of London
Conor McBride, University of Nottingham

Workshop Description

This one-day workshop will provide an introduction to dependent type theory. It is intended for post-graduate (Masters or PhD-level) students in Computer Science or related fields. No previous knowledge of or experience with type theory is required. By the end of the workshop, the participants will have received an overview of the history and current state of research in this field, and have received their first experience in using type theory for the formalisation of mathematics, and be aware of the current state of research into programming languages with dependent types.

This workshop is part of the TCS-SOUP series.

Date and Time

Date: Wednesday July 19th, 2006
Time: 09:30 - 16:00


Registration for this course is now closed. We are not accepting any more students for this course.

On arrival, students should report to the Arts Building (building 16 on the campus plan).


Royal Holloway, University of London is on the A30 between the village of Englefield Green and the town of Egham, 2 miles from junction 13 of the M25 and within walking distance of Egham train station.

The college boasts some spectacular architecture and a beautiful parkland campus, particularly in midsummer. An (optional) guided tour of the campus will be provided during the lunch session.

Travel directions


Campus Plan


Accommodation is not included but if you have far to travel and wish to arrange accommodation locally for the nights of 18th and/or 19th July, please be aware that cheap hotel/guest house rooms are very limited in the Egham area (Note: Royal Holloway is 20 miles west of central London).

Those who have booked a college guest room should check in at the temporary reception office (open 24 hrs) which is outside Williamson House (no. 40 on the Campus Plan), approximately opposite the Electron Microscopy Unit (no. 37 on the Campus Plan). Payment is due on arrival.


09:00 Welcome and Coffee

Arts Building Foyer (No. 16)
09:30 Introduction to Type Theory

Arts Building, Room G24 (No. 16)
11:00 Break
11:30 Formalisation of Mathematics

Tolansky Computer Science Laboratory (No. 22)
13:00 Lunch and Campus Tour

Mc Crae Building, Room 115 (No. 17)
14:30 Dependently Typed Programming

Arts Building, Room G24 (No. 16)
16:00 Close

Contact Details

For further information, contact the organisers:

Zhaohui Luo 01784 443431
Robin Adams 01784 443421

Return to department homepage

Page last updated 14 July 2006.