CS3 Language Semantics and Implementation

This course runs in Semester 2, on Mondays and Thursdays at 12.10-13.00 in room AT 2.11 (Monday) and DHT 4.01 (Thursday). Lecturers: Alex Simpson and Colin Stirling.

The syllabus of this course can be viewed in HTML at Syllabus
Tutorial: Exercises for the tutorials (which grows weekly)
Lecture Notes
- For the first 10 Lectures, Chapters 1-4 of the following notes by Andy Pitts of Cambridge University, ps.
- For lectures 11-12 on the language LLC (LC + let) see slides below for these lectures.
- Extra notes about induction ps, on natural numbers, lists, trees and abstract syntax by Gordon Plotkin
Lecture Slides
- Lecture 1, ps
- Lecture 2, ps
- Lectures 3 + 4, ps
- Lectures 5 + 6, ps
- Lectures 7 + 8, ps
- Lectures 9 + 10, ps
Further Reading
- Plotkin's original notes on structural operational semantics ps
- Abstract machines for programming language implementation This paper shows the vast variety of abstract machines for programming languages out there.
- Look at the proposal for a query language for XML. One of the defining documents is "XQuery 1.0 and XPath 2.0 Formal Semantics", which is written by Phil Wadler and others. It's available at: http://www.w3.org/TR/query-semantics and it uses operational semantics techniques for the language specification.
- M Hennessy (1990). ``The Semantics of Programming Languages'', Wiley. This book is actually available on the web here.
- Dynamic semantics of Java bytecode by Peter Bertelsen (13 pages), outlines a formalization of the Java Virtual Machine (JVM) and illustrates the approach for a few select JVM instructions.
- Semantics of Java Byte Code by Peter Bertelsen (67 pages), is the full version of the paper above.
- Machine-checking the Java Specification: Proving Type-Safety by David von Oheimb and Tobias Nipkow, provides an evaluation semantics for Bali, a subset of Java. Pretty difficult to read, but worth a look.
Lecture Log
1. Monday 11th January (cps): Introduction to operational semantics; Section 1.1 of Pitt's notes.
2. Thursday 14th January (cps): Most of the SMC machine; Section 1.2 of notes.
3. Monday 18th January (cps): Finished SMC machine; started induction, Section 2.1-2.3 of notes.
4. Thursday 21st January (cps): Finished structural induction and rule induction, Chapter 2 of notes.
5. Monday 25th January (cps): Defined `small-step' structural operational semantics for LC, Section 3.1 of notes.
6. Thursday 28th January (cps): Properties of `small-step' semantics, including proof of determinacy. Section 3.1 of notes.
7. Monday 1st February (cps): Introduced evaluation (big step) semantics for LC, Section 3.2 of notes.
8. Thursday 4th Feb (cps): Briefly outlined proof of equivalence between big-step and small-step semantics, Section 3.3 of notes. Discussed extensions of LC with print and parallel, comparing small-step and big-step semantics.
9. Monday 8th Feb (als): Introduced the evaluation relation for LC with block structure, Section 3.4. Covered semantic equivalence, Chapter 4.
Past Examination Papers

Colin Stirling, cps@inf.ed.ac.uk, January 2010.

Home : Teaching : Courses