DD2454 Semantics for Programming Languages 6.0 credits

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.

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.

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

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

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

Examination (TEN1; 6 university credits)

Dilian Gurov

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

Lectures: 20 h
Tutorials: 10 h.

The course is given every second year.

Registration for examination is required.