Skip to main content

DD2454 Semantics for Programming Languages 6.0 credits

To give a semantics for a programming language means to give a precise definition of the behaviour of programs written in this language. Only when the semantics of the language has been fixed, one can go about to prove such important properties like determinism and termination, equivalence of constructs, or that a given program meets its specification. Different semantic styles have been developed for different purposes, depending on the level of detail needed for the particular task. The most important ones are: operational semantics, denotational semantics and axiomatic semantics.

Course offering missing for current semester as well as for previous and coming semesters
Headings with content from the Course syllabus DD2454 (Autumn 2008–) are denoted with an asterisk ( )

Content and learning outcomes

Course contents

1. Operational Semantics: big-step semantics, small-step semantics and abstract machine semantics for the simple imperative language IMP.

2. Analysing IMP programs: state space exploration, termination, equivalence. Determinism of IMP.

3. Denotational Semantics for IMP. Fixed Point Theory. Relation with big-step operational semantics.

4. Axiomatic Semantics for IMP. Program Verification. Computing weakest preconditions.

5. Operational and denotational semantics for the simple declarative language REC. Domain Theory.

Intended learning outcomes

The overall aim of the course is to study the main semantic styles used for capturing the meaning of programs in a formal way, compare their strengths and weaknesses, and analyze how they can be used for establishing important properties of programming languages, concrete programs, and transformations on programs. A secondary goal is to learn the theories and proof techniques on which such semantic investigations are based.

After the course, the successful student will be able to perform the following constructions:

  • construct the state space of a program as a basis for program behaviour analysis through state space exploration;
  • compute the denotation of a program;
  • extend a programming language with new constructs, and extend its semantics accordingly;
  • specify and verify programs in Hoare logic,
  • formally 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.

For passing the course, a student has to demonstrate proficiency with problems of type 1-4; for the highest grade he/she has to be equally proficient at the remaining types of problems.

Course disposition

No information inserted

Literature and preparations

Specific prerequisites

No information inserted

Recommended prerequisites

No information inserted


No information inserted


Nielson and Nielson "Semantics with Applications: An Appetizer", Springer-Verlag, 2007, ISBN: 978-1-84628-691-9.

Examination and completion

If the course is discontinued, students may request to be examined during the following two academic years.

Grading scale

A, B, C, D, E, FX, F


  • TEN1 - Examination, 6.0 credits, grading scale: A, B, C, D, E, FX, F

Based on recommendation from KTH’s coordinator for disabilities, the examiner will decide how to adapt an examination for students with documented disability.

The examiner may apply another examination format when re-examining individual students.

Other requirements for final grade

Examination (TEN1; 6 university credits)

Opportunity to complete the requirements via supplementary examination

No information inserted

Opportunity to raise an approved grade via renewed examination

No information inserted


Profile picture Dilian Gurov

Ethical approach

  • All members of a group are responsible for the group's work.
  • In any assessment, every student shall honestly disclose any help received and sources used.
  • In an oral assessment, every student shall be able to present and answer questions about the entire assignment and solution.

Further information

Course web

No information inserted

Offered by

CSC/Computer Science

Main field of study

This course does not belong to any Main field of study.

Education cycle

Second cycle

Add-on studies

No information inserted


Dilian Gurov, tel: 790 8198, e-post:

Supplementary information

Lectures: 20 h
Tutorials: 10 h.

The course is given every second year.

Registration for examination is required.