Semantics of Programming Languages

Chair for Logic and Verification


Professor Prof. Tobias Nipkow
Lecture Monday 8:30-10:00 and Thursday 12:15-13:45 (pre-recorded)
Tutorial Monday 10:15-11:45 (remote or in person, depending on the circumstances)
First Lecture November 2, 2020
Language English
TUMonline IN2055
Submission System
Tutorial Sessions
Tutorial Organizers Fabian Huch





Homework is the heart and soul of this course. - Solved homework should be uploaded to the submission system, according to the instructions on the first exercise sheet. Make sure that your submission gets a “Passed” status in the system. We will not grade it otherwise! - The latest submission date is given on each exercise sheet. Late submissions will not be graded! If you have a good excuse (such as being very sick), you should contact the tutors before the deadline. - Each homework will get 0 to 10 points, depending on the correctness and quality of the solution. - Discussing ideas and problems with others is encouraged. When working on homework problems, however, you need to solve and write up the actual solutions alone. If you misuse the opportunity for collaboration, we will consider this as cheating. - Plagiarizing somebody else’s homework results in failing the course immediately. This applies for both parties, that is, the one who plagiarized, and the one who provided his/her solution. - Important: all homework is graded and contributes 50% towards the final grade.


The aim of this course is to introduce the structural, operational approach to programming language semantics. It will show how this formalism is used to specify the meaning of some simple programming language constructs and to reason formally about semantic properties of programs and of tools like program analyzers and compilers. For the reasoning part the theorem prover Isabelle will be used.

At the end of the course students should - be familiar with rule-based presentations of the operational semantics of some simple imperative program constructs, - be able to prove properties of an operational semantics using various forms of induction and - be able to write precise formal proofs with the theorem prover Isabelle.

Important Notice