Skolan för
och kommunikation
KTH / CSC / Kurser / DD2454 / semant08

Semantics for Programming Languages, semant08

DD2454 Semantics for Programming Languages

Latest News

  • If you haven't already done this in class, please print and fill in the following anonymous course evaluation sheet and put it in my mailbox.

Course Literature

course bookNielson and Nielson
Semantics with Applications: An Appetizer
Springer-Verlag, 2007, ISBN: 978-1-84628-691-9
Available from Kårbokhandeln at the start of the period.

In addition: some hand-written slides on axiomatic semantics and verification condition generation (see outline, part III).

Additional reading for the curious student:
  • a paper by Freund and Mitchell formalizing the Java Virtual Machine and Language, thus providing an abstract machine semantics for the Java bytecode language JVML.

Course Structure

For formal reasons, the teaching is divided into lectures (F) and tutorials (Ö), but in fact there will be some kind of "lektionsundervisning", where theory and examples are mixed.

Here is the course schedule. The following course outline will follow the material already covered, and suggest reading and exercises, both based on the course book.


The assignments will typically consist of a number of exercises taken from the textbook. They will be checked in class by peer reviewing, with the help of solutions provided by the lecturer, and be collected by the lecturer. At least 60% of all assignments have to be handed in as a prerequisite to admission to the final exam. Each assignment handed in on time will contribute a bonus point for the final exam (which will consist of ca. 30 points).


The requirement for the course is a pass on the written exam. The grade will be the grade obtained at the exam. You're allowed to bring the course book, hand-outs and own lecture notes taken in class.

Note that you must be registered for the course in order to have the result of your exam reported.

Exam resits

Exam resits (sv. omtentor) are by mutual arrangement with the lecturer.


The exam will be graded based on the intended learning outcomes of the course. The successful student will be able to perform constructions such as:
  • Construct the state space of a program as a basis for program behaviour analysis through state space exploration.
  • Translate programs to abstract machine code, and execute the latter.
  • Compute the denotation of a program.
  • As above, but in abstract domains.
  • Extend a programming language with new language features, and extend its semantics and abstract machine implementations accordingly.
  • Suggest and justify program transformations, supported by a suitable program analysis. 
  • Specify and verify programs in Hoare logic.
  • Generate verification conditions from a program with annotated while loops.
As well as be able to formally establish results such as:
  • Relate different semantic styles.
  • Prove language properties such as determinism and termination.
  • Show correctness of a given program transformation by proving equivalence of the original and the transformed program.
  • Show properties of a given semantics.
For passing the course, a student has to demonstrate proficiency with problems of the first type; for the highest grade he/she has to be equally proficient at the remaining types of problems.

Bonus points will be taken into account, namely one bonus point per homework assignment handed in on time.

Course Board (sv. Kursnämnd)

A course board is a formal way for students to influence the content and form of the education. It is formed at the beginning of the course.

Course Evaluation and Analysis

A course evaluation is performed after the course to give input for improvements for later versions of the course. Here is the latest course analysis (in Swedish).

Copyright © Sidansvarig: Dilian Gurov <>
Uppdaterad 2008-08-29