Types and Semantics for Programming Languages

Course feedback


10.00–10.50 Monday (lecture)
11.10–12.00 Monday (tutorial)
10.00–10.50 Thursday (lecture)
11.10–12.00 Thursday (tutorial)
10.00–10.50 Friday (lecture)
11.10–12.00 Friday (tutorial)

All lectures and tutorials in AT 5.08.

Note: Lectures begin Monday of Week 1.


Coursework is worth 25% of your mark. There are five coursework assignments, each worth 5%.

For each assignment you will be given a list of exercises to complete in the textbook. Copy the relevant files and fill in your answers. Include a comment at the beginning, listing your name and which exercises you completed. Mark every completed exercise by writing (* !!! *) just before it. E-mail your files to the instructor. Send all relevant files: .v, .vo, and .glob. Please ensure your files execute correctly under Coq!

Some exercises are labeled 'stretch'. These are optional exercises for students who wish an additional challenge.

Note: The coursework is not a light load! But everyone who does the work gets perfect on the exam. (Literally. 100%. That's what proof is for.)

Second mock exam

Good scholarly practice

Please remember the University requirement as regards all assessed work. Details about this can be found at:


Furthermore, you are required to take reasonable measures to protect your assessed work from unauthorised access. For example, if you put any such work on a public repository then you must set access permissions appropriately (generally permitting access only to yourself, or your group in the case of group practicals).

Lecture log

Past papers

Go here and click on the link for past papers "Exam papers for academic sessions 2004/05 - 2016/17". Then search for "Types and Semantics".

To attempt a past paper, use Exam.v and Maps.v from Assignment 5.


AT-5.08 South Lab on Thursday 14 December 09:30-11:30

The final examination is worth 75% of your mark.

Because you will be working with Coq throughout the course, you should also have access to Coq for the exam. Unlike most courses with a written exam, TSPL has an online exam where you use the Coq proof assistant to assist and confirm your exam work. If anyone has any questions or concerns, please contact the instructor.

The final exam for TSPL is in December 2017

Home : Teaching : Courses 

Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland, UK
Tel: +44 131 651 5661, Fax: +44 131 651 1426, E-mail: school-office@inf.ed.ac.uk
Please contact our webadmin with any comments or corrections. Logging and Cookies
Unless explicitly stated otherwise, all material is copyright © The University of Edinburgh