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 (in-person + live-stream
Tutorial Tuesday 14:00-16:00 (in-person)
First Lecture/Tutorial October 20 / October 25
Language English
TUMonline Course IN2055
Submission System Proving for Fun
Discussion Platform Zulip streams: Announcements and Discussion
Tutorial Organizers Fabian Huch
Exam 15.2., 14:15 to 16:15, MW 1350, Ludwig-Burmester-Zeichensaal (5503.01.350))


We will write the exam using Isabelle, with the known submission system - bring your laptop! All course material (book, slides, sheets, theories) is allowed. During the exam, you may only use the internet to submit your solution.



Homework is the heart and soul of this course.


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:

Important Notice