Semantics of Programming Languages

Chair for Logic and Verification

Overview

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)
First Lecture November 2, 2020
Language English
TUMonline IN2055
Moodle https://www.moodle.tum.de/course/view.php?id=57941
Submission System https://competition.isabelle.systems
Piazza piazza.com/tum.de/winter2021/in2055
Tutorial Sessions https://bbb.rbg.tum.de/fab-k3t-f7g
Tutorial Organizers Fabian Huch

News

Material

Exercises

Exercise 1 2.11.2020 - 8.11.2020 exercise sheet
Exercise 2 9.11.2020 - 15.11.2020 exercise sheet, thy file
Exercise 3 16.11.2020 - 22.11.2020 exercise sheet, thy file
Exercise 4 23.11.2020 - 29.11.2020 exercise sheet, thy file
Exercise 5 30.11.2020 - 6.12.2020 exercise sheet, thy file
Exercise 6 7.12.2020 - 13.12.2020 exercise sheet, thy file
Exercise 7 14.12.2020 - 20.12.2020 exercise sheet, thy file
Exercise 8 21.12.2020 - 10.1.2021 exercise sheet, thy file
Exercise 9 11.1.2021 - 17.1.2021 exercise sheet, thy file
Exercise 10 18.1.2021 - 24.1.2021 exercise sheet, thy file
Exercise 11 25.1.2021 - 31.1.2021 exercise sheet, thy file
Exercise 12 1.2.2021 - 7.2.2021 exercise sheet, thy file

Homework

Homework is the heart and soul of this course.

Aims

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

Literature