University Homepage School Homepage School Contacts School Search

CS3 Language Semantics and Implementation

THIS IS LAST YEARS WEB PAGE: course will run Monday and Thursdays, 12.10-13.00 in semester 2, 2009-10.

This course runs in Semester 2, on Tuesdays and Fridays at 10.00-10.50 in room 4.07 (tuesday) and 4.12 (friday) in Appleton Tower. Lecturers: Alex Simpson and Colin Stirling.

• The syllabus of this course can be viewed in HTML at Syllabus

• Tutorial
• 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
  • Lectures 11 + 12, ps
  • Lectures 13 + 14, ps
  • Lectures 15, ps
  • Revision Lecture, 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. Tuesday 13th January (cps): Introduction to structural operational semantics; Section 1.1 of Pitt's notes.
  2. Friday 16th January (cps): Most of the SMC machine; Section 1.2 of notes.
  3. Tuesday 20th January (cps): Finished SMC machine; started induction, Section 2.1-2.3 of notes.
  4. Friday 23rd January (cps): Finished structural induction and rule induction, Chapter 2 of notes.
  5. Tuesday 27th January (als): Defined `small-step' structural operational semantics for LC, Section 3.1 of notes.
  6. Friday 30th January (als): Properties of `small-step' semantics, including proof of determinacy. Section 3.1 of notes.
  7. Tuesday 3rd February (als): Introduced evaluation (big step) semantics for LC, Section 3.2 of notes. Stated equivalence between big step and small step.
  8. Friday 6th Feb (als): 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. Announced availability of first coursework exercise on web.
  9. Tuesday 10th Feb (cps): Introduced the evaluation relation for LC with block structure, Section 3.4, and started semantic equivalence, Chapter 4.
  10. Friday 13th Feb (cps): Semantic equivalence. Chapter 4 of notes.
  11. Tuesday 17th Feb (cps): Application of semantics to logic of partial correctness. Semantics of LLC (LC+let) and definition of substitution (see slides).
  12. Friday 20th Feb (cps): Finished semantics of LLC with adding parameters (see slides).
  13. Tuesday 24th Feb (als): Introduced LFP(+), its evaluation semantics, and recursion operator. This is covered in Sections 5.1,5.2 and 5.4 of notes, but our treatment is different in some details.
  14. Friday 27th Feb (als): Covered static semantics for LFP+, and statements of subject reduction and cbn side-effect freeness. Announced availability of second coursework exercise on web.
  15. Tuesday 3rd March (als): Alpha-equivalence, general substitution and semantic equivalence for LFP+.
  16. Friday 6th March (als): Revision lecture.

• Coursework
  • Exercise 1 (pdf, ps)
    Deadline: noon, Monday 23rd February
  • Exercise 2 (pdf, ps)
    Deadline: noon, Monday 16th March

• Past Examination Papers

---

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