Semantics of Programming Languages

Dr. Peter Lammich, Prof. Tobias Nipkow, Wintersemester 2014/15

The course is based on this new book.

On this page: News Lecture and Exercises Homework Aims Important notice Literature



  • Book: Concrete Semantics including slides and demo theories
  • All IMP theories are in the Isabelle distribution in src/HOL/IMP. You can import theory T like this: imports "~~/src/HOL/IMP/T"



Homework is the heart and soul of this course.


The aim of this course will be 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