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 7.3.2023.
Lecture/exercise/examen dates for the summer term 2023
Every Tuesday, Thursday, 10:00-12:00
Schedule
2.3. no lecture
7.3. Q&A 1 (first-order-logic/intro/lecture1)
9.3. Q&A 2 (lecture2)
14.3. FO-exercise sheet/ repetition-sheet
16.3. Q&A 3 (lecture3)
21.3. Q&A 4 (lecture4)
23.3. exercise 1
28.3. Q&A 5 (lecture5)
30.3. exercise 2
4.4. Osterferien
6.4. Osterferien
11.4. Osterferien
13.4. Osterferien
18.4. no lecture
20.4. Q&A 6 (lecture6)
25.4. exercise 3
27.4. Q&A 7 (lecture7)
2.5. Q&A 8 (lecture8)
4.5. exercise 4
16.5. no lecture
18.5. Christi Himmelfahrt
23.5. Q&A 9 (lecture9)
25.5. tba
30.5. TU Pfingstferien
1.6. exercise 5
6.6.
8.6. Fronleichnam
13.6. exam
15.6.
20.6.
22.6.
27.6.
29.6.
Lecture mode:
We plan for a flipped-classroom setting with pre-recorded videos and Q&A sessions in the calssroom. (If the majority of the students prefers live lectures, we can however switch to in-classroom lectures. This will be determined at the first lecture date on 7.3. For the 7.3. the students are asked to watch the three videos specified for this date.)
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 7th, 2023, in which the lecture mode will also be discussed again. (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.
