CS3 Language Semantics and Implementation

• 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 http://www.cl.cam.ac.uk/Teaching/2000/Semantics/
  • 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)
  • Lectures 1 + 2
  • Lecture 3
  • Lecture 4
  • Lecture 5
  • Lecture 7
  • Lecture 8
  • Lecture 9: LLC slides
  • Lecture 10: static semantics
  • Lecture 11: records
  • Lecture 12: parameters
  • Lecture 13 and 14: syntax and semantics of LFP
  • Lecture 17: semantics of the Java Virtual Machine
  • Lecture 18: some remarks on a evaluation semantics for Java

• Further Reading
  • Plotkin's original notes on structural operational semantics
  • Notes by Kevin Mitchell for the course from previous years
  • Featherweight Java by Igarashi, Pierce and Wadler;
  • G Winskel (1993). ``The Formal Semantics of Programming Languages'' MIT Press
  • M Hennessy (1990). ``The Semantics of Programming Languages'', Wiley.
  • 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
  • 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, 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.

• Coursework
  • Exercise 1
  • Exercise 2
  • Exercise 3

• Past Examination Papers