After successful completion of the course, students are able to...
- to specify the semantics of new programming constructs.
- to prove the correctness of a program using the programming language semantics.
- to compare the different ways of specifying the semantics of a programming language and choose the appropriate semantics for the problem at hand.
- to conduct proofs about the semantics of a programming language, choosing the appropriate induction techniques.
The lecture introduces the different techniques for defining the semantics of a programming language. While the syntax of a programming language defines which programming constructs are available in the language, the semantics determines the meaning of these constructs. In semantics, we use techniques from mathematics in oder to precisely and concisely define the meaning of programming constructs. The semantics of a programming language is the basis for arguing about wether a program does what we expect from it. For example, a precise definition of the semantics is necessary for arguing whether a compiler correctly translates C-programs into assembly language (see the CompCert project, http://compcert.inria.fr/) or to prove that a program is functionally correct and free from certain types of errors (see the seL4 Microkernel project, https://sel4.systems/, which ensures the absence of buffer-overflows and other errors.) An example for current research in semantics are correctness criteria for modern multi-core processors that can reorder memory reads and writes for efficiency reasons (siehe https://en.wikipedia.org/wiki/Memory_ordering).
In the lecture we discuss
- the operational, denotational and axiomatic semantics of a simple imperative programming language.
- the relationship between the different types of semantics (operational, denotational and axiomatic).
- mathematical proof techniques for arguing about the semantics of a program, in particular using proofs by induction.
- selected topics such as non-determinism and concurrency.
- how to prove the correctness of a compiler.
- the operational semantics and the type system of a simple functional programming language, and the correctness of the type system with regard to the operational semantics.
The course consists of lectures + 5 exercise sessions.
In the exercise sessions the students engage actively with the material from the lecture. For each exercise session the student prepare an exercise sheet. Solving the exercises from the exercise sheets, the students learn
- to specify the semantics of new programming constructs.
- to prove the correctness of a program using the programming language semantics.
- to compare the different means of specifying the semantics of a programming language and use the appropriate semantics for the problem at hand.
- to conduct proofs about the semantics of a programming language, choosing the appropriate induction techniques.
ECTS Breakdown: ECTS 4.5 = 112h
Lectures: 8 Units of 5 hours each: 40 Std
Exercises: 50 Std
Exam (including preparation time): 22 Std
Start: The course starts on 8.3.2022.
Lecture/exercise/examen dates for the summer term 2022
Every Tuesday, 12:00-14:00
Schedule
8.3. Q&A 1 (first-order-logic/intro/lecture1)
15.3. FO-exercise sheet/ repetition-sheet
22.3. Q&A 2 (lecture2/lecture3)
29.3. exercise 1
5.4. Q&A 3 (lecture4/lecture5)
12.4. Easter Holidays
19.4. Easter Holidays
26.4. exercise 2
3.5. Q&A 4 (lecture6/lecture7)
10.5. exercise 3
17.5. Q&A 5 (lecture8/lecture9)
24.5. exercise 4
31.5. tba
7.6. Pentecost Holidays
14.6. exercise 5
21.6. tba
28.6. exam
Lectures and slides will be videotaped in advance and posted online. The students are asked to watch the videos independently in advance. Questions about the lectures can be discussed in the Q&A sessions. The videos discussed in the Q&A sessions are indicated in the brackets of the respective Q&A session. In order to be able to view the teaching materials, it is necessary to register for the lecture. There are 5 exercise sheets + an extra exercise sheet on first-order logic, which are to be solved in advance and to be presented in the practice sessions (by ticking the prepared exercises). The lecture begins with the Q&A session on March 8th, 2022, in which the lecture mode will also be discussed again. It is planned to hold the Q&A sessions + practice + exam sessions in person, if necessary due to the pandemic, we will switch to online classes. (Note that the lecture recordings are from SS2021. Hence, the dates in the lecture recordings are not correct.)
------
Further Reading:
"Introduction to lattices and order", B. A. Davey and H. A. Priestley is a good introduction to lattice theory
"Types and Programming Languages", Benjamin Pierce is the standard introduction into types in programming languages
Basic knowledge of first-order logic (FOL) as introduced in the courses 185.278 and 185.291; in particular, understanding the difference between syntax and semantics and being able to use structural induction for proving properties of FOL formulae.
Basic knowledge of Hoare-logic as introduced in185.291.
Working knowledge of set-theoretic and logical notation; in particular, being able to precisely formulate and prove mathematical statements as taught and practiced in the coureses 104.271, 185.278, 185.291.