Semantics of Programming Languages

Overview

Organization

• Announcements will be made on Zulip (Announcements stream).
• Before attending the tutorial, you should study and listen to the preceding lecture’s material
• Both the lecture and tutorial will take place in-person. The lecture cannot be recorded/streamed, but there recordings from 2023.
• Exercises
• There will be no resit / Wiederholungsprüfung!
• The exam will be written in person using Isabelle on your own laptop. All lecture material (lecture slides and the book, homeworks, tutorial, your notes) may be used.

Material

• Book: Concrete Semantics including slides and demo theories
• Some motivational slides
• Exercises

Homework

• Doing the homework is essential to successfully complete the course.
• Important: all homework is graded and contributes 50% towards the final grade.
• Solved homework should be uploaded to the submission system, according to the instructions on the first exercise sheet. Make sure that your submission gets a “Passed” status in the system. We will not grade it otherwise!
• The submission date is given on each exercise sheet. Late submissions will not be graded! If you have a good excuse (such as being very sick), you should contact the tutors before the deadline.
• Each homework will get 0 to 10 points, depending on the correctness and quality of the solution.
• Discussing ideas and problems with others is encouraged (particularly on Zulip). When working on homework problems, however, you need to solve and write down the actual solutions alone. If you misuse the opportunity for collaboration, we will consider this as cheating.
• Plagiarizing somebody else’s homework results in failing the course immediately. This applies to both parties, that is, the one who plagiarized and the one who provided their solution.

Aims

The aim of this course is to understand the foundations of programming language semantics and use it to formally specify and prove correct properties about (simple) programming languages and programs. We will explore different approaches to specify the semantics of programming languages (operational, denotational, axiomatic). We will reason formally about semantic properties of programs and programing languages using the Isabelle proof assistant. We will also derive and prove correct simple program analyzers and compilers using Isabelle.

At the end of the course students should:

• be familiar with rule-based presentations of the semantics of program languages,
• be able to prove properties of programs and programming languages using various forms of induction, and
• be able to write precise formal proofs with the proof assistant Isabelle.

Important Notes

• You must be familiar with the basics of some functional programming language like Haskell, Objective Caml, Standard ML or F# (as taught, for example, in Functional Programming and Verification (IN0003)). For motivated students who do not have the necessary background yet: There are many introductions to functional programming available online, for example the first 6 chapters of Introduction to Objective Caml.
• You must haven taken some basic course in discrete mathematics and feel at ease with sets, relations, and proof principles like induction (as taught, for example, in Discrete Structures (IN0015)).
• You need not be familiar with formal logic, but you must be motivated to learn how to write precise and detailed mathematical proofs that are checked for correctness by a machine, the theorem prover Isabelle.
• At the end of the course there will be a written, oral, or remote examination, depending on the number of students. Throughout the course there will be homework assignments. They will involve the use of Isabelle and will be graded. The final grade will be a combination of the examination and the homework grades, though you need to pass the exam.
• You must be subscribed to the Zulip Announcements stream. All announcements will be made there.
• Please install Isabelle 2024 from the website and run it once before the fist tutorial.

Literature

• The primary reference: Tobias Nipkow, Gerwin Klein: Concrete Semantics with Isabelle/HOL
• Two traditional alternatives not based on proof assistants:
  • Hanne Riis Nielson, Flemming Nielson: Semantics with Applications: A Formal Introduction.
  • Glynn Winskel: The Formal Semantics of Programming Languages. MIT Press.