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 1-4 of
the following notes by Andy Pitts of Cambridge University, see
- For lectures 9-11 see the slides below
- For lectures 12-16 Chapter 5 of Andy Pitt's notes
- For lectures 17-18 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
- 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
- Tuesday 12th Feb: Records, pi-types, 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. Call-by-name and call-by-value.
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.
Colin Stirling, firstname.lastname@example.org, JCMB room 3422, January 2002.