To give a semantics for a programming language means to give a precise definition of the behaviour of programs written in this language. Once the semantics of the language has been described formally, one can go about and prove various language properties like determinism, prove correctness of program implementations based on abstract machines, justify various program analyses used in syntax-oriented editors and program transformations used in optimising compilers, and specify and prove correctness of concrete programs. This provides the formal basis for a variety of software tools for program analysis, optimisation and verification.
Information for research students about course offerings
The course is offered every other year in period 4.
Content and learning outcomes
Part I. Operational Semantics and Language Implementation: natural semantics, structural operational semantics, abstract machines, correctness of language implementation.
Part II. Denotational Semantics and Program Analysis: denotational semantics, fixed-point theory, program analysis and transformation.
Part III. Axiomatic Semantics and Program Verification: axiomatic semantics, program specification and verification, weakest pre-conditions, verification condition generation.
Intended learning outcomes
After completing the course, the successful doctoral student should be able to:
- Account for the main semantic styles used for capturing the meaning of programs in a formal way, both in theory and on examples.
- Relate different semantic styles, and compare their strengths and weaknesses.
- Use these semantic styles for program analysis, optimisation and verification, both in theory and as a basis for software tools.
- Extend a programming language with new language features, and extend its semantics accordingly.
- Prove formally properties of a given semantics.
The course consist of lectures, lab sessions, a seminar and a written final exam. There are six homeworks, which are peer-reviewed in class, and two laboratory assignments.
Literature and preparations
Courses in Programming, Discrete Mathematics, and Mathematical Logic.
Nielson and Nielson "Semantics with Applications: An Appetizer", Springer-Verlag, 2007, ISBN: 978-1-84628-691-9. Research papers.
Examination and completion
If the course is discontinued, students may request to be examined during the following two academic years.
- EXA1 - Examination, 7.5 credits, grading scale: P, 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
To pass the course, doctoral students need to pass the homework assignments, the laboratory assignments, the seminar, and the written exam.
Opportunity to complete the requirements via supplementary examination
Opportunity to raise an approved grade via renewed examination
- 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 about the course can be found on the Course web at the link below. Information on the Course web will later be moved to this site.Course web FDD3557