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 3.3.2020.

Lecture/exercise/examen dates for the summer term 2020

3.3. intro/lecture-FO-part1
5.3. lecture-FO-part2/ex-FO online
10.3. lecture1
12.3. lecture2/ex1 online
17.3. exercise-FO
19.3. repetition
24.3. lecture3/ex2 online
26.3. TBA
31.3. lecture4
2.4. exercise1
7.4. Easter Break
9.4. Easter Break
14.4. Easter Break
16.4. Easter Break
21.4. lecture5/ex3 online
23.4. TBA
28.4. exercise2
30.4. lecture6
5.5.   TBA 
7.5. lecture7/ex4 online
12.5. lecture8
14.5. exercise3
19.5. lecture9/ex5 online
21.5. Public Holiday (Christi Himmelfahrt)
26.5. exercise4
28.5. TBA
2.6. University Holiday (Pfingstferien)
4.6. exercise5
9.6.
11.6. Public Holiday (Fronleichnam)
16.6. exam
18.6.
23.6.
25.6.
30.6. if needed: exam repetition

------

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

At the end of the term, there is a written 2h exam (open-book). The exam questions are similar to the exercises of the exercise sheets.

None.

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.