Semantics of Programming Languages

Chair for Logic and Verification

Overview

Professor Prof.Ā Tobias Nipkow
Lecture Tuesday 14:15-15:45 and Wednesday 08:30-10:00 im Galileo (8120.EG.001)
Tutorial Thursday 10:15-12:00
First Lecture/Tutorial October 15 / October 17
Language English
TUMonline Course IN2055
Submission System Proving for Fun
Discussion Platform Zulip streams: Announcements and Discussion (or subscribe via the Isabelle emoji)
Tutorial Organizers Lukas Stevens, Kevin Kappelmann (mailto: semantics@proof.cit.tum.de)
Exam Thursday Feb 27, 17:00-19:00, 0001, ZEI-Seminarraum (5414.EG.001)

Organization

Material

Homework

Exam

Exam PDF
Solution PDF

The exam grade is calculated from the percentage of the points you achieved in the exam and the homework exercises, where the maximum number of points in the exam is 40 and in the homework exercises 141. The formula to calculate the total percentage is

0.5 * min((exam points / 40) * 100 + 15, 100) + 0.5 * min((homework points / 141) * 100, 100)

where we add 10 percentage points to the exam percentage to account for its difficulty. The overall grade is determined by the grading key below.

Percentage Grade
0 5
13 4.7
26 4.3
40 4
46 3.7
52 3.3
58 3
64 2.7
70 2.3
76 2
82 1.7
88 1.3
94 1

Aims

The aim of this course is to understand the foundations of programming language semantics and use it to formally specify and prove correct properties about (simple) programming languages and programs. We will explore different approaches to specify the semantics of programming languages (operational, denotational, axiomatic). We will reason formally about semantic properties of programs and programing languages using the Isabelle proof assistant. We will also derive and prove correct simple program analyzers and compilers using Isabelle.

At the end of the course students should:

Important Notes

Literature