184.749 Semantics of Programming Languages
This course is in all assigned curricula part of the STEOP.
This course is in at least 1 assigned curriculum part of the STEOP.

2021S, VU, 3.0h, 4.5EC

Properties

  • Semester hours: 3.0
  • Credits: 4.5
  • Type: VU Lecture and Exercise
  • Format: Distance Learning

Learning outcomes

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.

Subject of course

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.

Teaching methods

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.

Mode of examination

Written

Additional information

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

Lecturers

Institute

Examination modalities

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.

Course registration

Begin End Deregistration end
12.02.2021 09:00 25.04.2021 22:00 26.05.2021 22:00

Registration modalities

None.

Curricula

Literature

No lecture notes are available.

Previous knowledge

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.

 

Preceding courses

Language

English