Types and Semantics for Programming Languages


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

All lectures and tutorials in FH 1.B31.

Note: Lecture begin in Monday of Week 2.


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 and third mock exams

Good scholarly practice

Please remember the University requirement as regards all assessed work for credit. Details about this can be found on here.

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).

Lecture log


Past exam papers

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.

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