Semantics of Programming Languages

Overview

News

• Given the current situation, the tutorial will take place as a remote session.
• Links to the tutorial BBB recordings are on moodle. If you need access to the moodle course, write an email to {huch} AT [in.tum.de].
• The final exam will be held online. It will consist of two parts:
  1. Isabelle part, using the submission system
  2. Theoretical part, which can be submitted either as comment within the theory file or as a scan or (readable) photo of your worksheet
• The exam will take place in the BBB room. An online exam test run will be held on Monday, 15.2., in the usual tutorial time slot.

Material

• Book: Concrete Semantics including slides and demo theories
• Lecture videos. We will reuse many of the recordings from 2019 together with some new recordings from 2020 (→ IN2055: Semantics of Programming Languages)
  • 2.11.2020: watch 17.10.2019 and the first 58 minutes of 21.10.2019; read Sections 2.1 and 2.2 (in the book).
  • 5.11.2020: watch the rest of 21.10.2019 and all of 24.10.2019; read the rest of Chapter 2.
  • 9.11.2020: watch 28.10.2019; read Chapter 3.
  • 12.11.2020: watch 31.10.2019; read Sections 4.1 - 4.4.
  • 16.11.2020: watch 4.11.2019 read Sections 4.5 and 5.1-5.3.
  • 19.11.2020: watch 7.11.2019 up to 1:24:30, the end of Part I; read Section 5.4.
  • 23.11.2020: watch the end of 7.11.2019 and all of 11.11.2019; read Sections 7.1 and 7.2 up to and including 7.2.4.
  • 26.11.2020: watch 14.11.2019 and the first few minutes of 14.11.2019 up to but excluding Chapter 8; read the rest of Chapter 7.
  • 30.11.2020: watch 18.11.2019; read Chapter 8 excluding the second direction of the compiler correctness proof.
  • 3.12.2020: watch 21.11.2019; read the intro to Chapter 9 and all of Section 9.1.
  • 7.12.2020: watch 25.11.2019 and the first few minutes of 28.11.2019 up to but excluding Chapter 10; read Section 9.2.
  • 10.12.2020: watch Definite Assignment Analaysis; read the intro to Chapter 10 and all of Section 10.1.
  • 14.12.2020: watch Live Variable Analysis; read Section 10.3. and the beginning of 10.4.
  • 17.12.2020: watch 5.12.2019 starting from the Knaster-Tarski theorem; read the rest of 10.4 and the beginning of Chapter 11 up to but excluding 11.1.1.
  • 21.12.2020: watch 9.12.2019; read the rest of Chapter 11 and the beginning of Chapter 12 up to but excluding 12.2.
  • 7.1.2021: watch Hoare Logic; read up to the beginning of but excluding 12.3.1.
  • 11.1.2021: watch Hoare Logic Completeness; read up to the beginning of but excluding 12.4.
  • 14.1.2021: watch the end of 16.12.2019 starting at 1:02:40, watch 19.12.2019; finish reading Chapter 12.
  • 18.1.2021: watch 9.1.2020; read the beginning of Chapter 13 up to but excluding 13.3.2.
  • 21.1.2021: watch 13.1.2020; read up to but excluding 13.4.2.
  • 25.1.2021: watch 16.1.2020; read up to but excluding 13.5.5.
  • 28.1.2021: watch 20.1.2020; read up to but excluding 13.7.
  • 1.2.2021: watch 23.1.2020 up to 1:12:33; read 13.7.
  • 4.2.2021: watch Interval Analysis; download new, corrected version of slides; read 13.8.
  • 8.2.2021: watch 30.1.2020; read 13.9.
• Old exam, solution. Of course this years exam will be a bit different due to the new format.

Exercises

Homework

Homework is the heart and soul of this course.

• 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 latest 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. When working on homework problems, however, you need to solve and write up 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 for both parties, that is, the one who plagiarized, and the one who provided his/her solution.
• Important: all homework is graded and contributes 50% towards the final grade.

Aims

The aim of this course is to introduce the structural, operational approach to programming language semantics. It will show how this formalism is used to specify the meaning of some simple programming language constructs and to reason formally about semantic properties of programs and of tools like program analyzers and compilers. For the reasoning part the theorem prover Isabelle will be used.

At the end of the course students should:

• be familiar with rule-based presentations of the operational semantics of some simple imperative program constructs,
• be able to prove properties of an operational semantics using various forms of induction and
• be able to write precise formal proofs with the theorem prover Isabelle.

Important Notice

• 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 Introduction to Informatics 2 (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 where you learned about 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.

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.