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

Lecture/exercise/examen dates for the summer term 2021

Every Tuesday, 13:00-15:00

Schedule

23.3. Q&A 1 30.3. Easter Holidays 6.4. Easter Holidays 13.4. FO-exercise sheet/ repetition-sheet 20.4. Q&A 2 27.4. exercise 1 4.5. Q&A 3 11.5. exercise 2 18.5. Q&A 4 25.5. Pentecost Holidays 1.6. exercise 3 8.6. Q&A 5 15.6. exercise 4 22.6. exercise 5 29.6. exam

Lectures will be pre-recored. The lecture date will be used for Q&A sessions about the lecture content and discussion of the exercises. The exact modalities will be discussed on the first date on 23.3.2021. Lecture slides from the previous year have already been put online (these slides might be updated in the current term).

------

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 an oral exam (with whiteboard) via Zoom. 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.