CS3 Language Semantics and Implementation
This module runs in term 2, on Tuesdays at 9am in JCMB Lecture Theatre C
and on Fridays at 9am also in JCMB Lecture Theatre C.

Syllabus of this module can be viewed in HTML through the
CS3 Course Guide
 Tutorial Groups. Tuesdays at 12.00
 Lecture Notes
 For the first 8 Lectures, Chapters 14 of
the following notes by Andy Pitts of Cambridge University, see
http://www.cl.cam.ac.uk/Teaching/2000/Semantics/
 For lectures 911 see the slides below
 For lectures 1216 Chapter 5 of Andy Pitt's notes
 For lectures 1718 see the slides below
 Extra Slides (not in the lecture notes)
 Further Reading
 Lecture Log
 Tuesday 8th Jan: Introduction to structural operational semantics
Section 1.1 of Pitt's notes.
 Friday 11th Jan: The SMC machine, Sections 1.2 and 1.3
of notes.
 Tuesday 15th Jan: Induction, structural induction and rule induction. Chapter 2 of notes.
 Friday 18th Jan: Transition semantics of LC. Section 3.1 of notes.
 Tuesday 22nd Jan: Evaluation semantics of LC. Section 3.2 of notes.
First exercise handed out (available below).
 Friday 25th Jan: Proof of equivalence of
LC transition and evaluation semantics.
 Tuesday 29th Jan: Hoare logic as an example of application of the evaluation
semantics. An evaluation rule for block structures.
 Friday 1st Feb: Block structures continued. Definition of semantic equivalence.
Proof of the congruence property for semantic equivalence.
 Tuesday 5th Feb: Introduction of the the language LLC, LC
with the let construct. See LLC slides.
 Friday 8th Feb: Static semantics of LLC. See static semantics
slides.
 Tuesday 12th Feb: Records, pitypes, classes and objects.
See record slides. Second exercise handed out (available below).
 Friday 15th Feb: adding parameters. See parameter slides.
 Tuesday 19th Feb: the LFP language. Section 5.1 of notes.
 Friday 22th Feb: evaluation semantics. Callbyname and callbyvalue.
Section 5.2 of notes.
 Tuesday 26th Feb: static semantics of LFP. Section 5.3 of notes.
 Friday 1st March: adding recursion to LFP: the LFP+ language. Section 5.4 of notes.
Third exercise handed out (available below).
 Tuesday 5th March: An operational semantics for the Java Virtual Machine. See slides
and Bertelsen's entries in Further Reading.
 Coursework
 Past
Examination Papers
Colin Stirling, cps@dcs.ed.ac.uk, JCMB room 3422, January 2002.