University Homepage School Homepage School Contacts School Search

CS3 Language Semantics and Implementation

This course runs in Semester 2, on Mondays and Thursdays at 12.10-13.00 in room 110 at 24 Buccleuch Place. Lecturers: Richard Mayr and Colin Stirling.

• The syllabus of this course can be viewed at Syllabus

• Lecture Notes
  • For the first 10 Lectures, Chapters 1-4 of the following notes by Andy Pitts of Cambridge University, and for Lectures 13-16, Chapter 5.
  • Extra notes about induction ps, on natural numbers, lists, trees and abstract syntax by Gordon Plotkin

• Lecture Slides

• 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 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

• Graded Coursework:
  
  • Coursework 1
    • To be submitted: THURSDAY 27th February at 4.00pm to the ITO
    • When available online: before Friday 10th November
    • When marked with written feedback: by Thursday 13th March
  • Coursework 2
    • To be submitted: MONDAY 24th March at 4.00pm to the ITO
    • When available online: before Friday 7th March
    • When marked with written feedback: by Monday 7th April

• Past Examination Papers

---

Colin Stirling, cps@inf.ed.ac.uk, September 2013.