Semantics of Programming Languages

Prof. Tobias Nipkow, Wintersemester 2017/18

The course is based on this book.

On this page: News Lecture and Exercises Homework Aims Important notice Literature

News

  • 06.12.: A mistake in Homework 8.2 has been fixed. Please re-read the overview at the beginning of the exercise.
  • 22.11.: A small mistake in Step 1 of Homework 6.2 has been fixed. The theorem exec_equiv_bigstep should contain a quantification over f, not i.
  • 10.11.: Deadline for Sheet 4 has been extended to Nov 21.
  • 10.11.: There is no tutorial in the week of Nov 13 to Nov 17.
  • 27.10.: Sheet 3 has been published: Submission deadline is Tuesday, Nov 7.
  • 24.10.: Sheet 2 has been updated: New submission deadline is Thursday, Nov 2.
  • 20.10.: Homework submission is now available.
  • 20.10.: We have created a discussion forum on Piazza: Ask questions about the course there.
  • Please bring your laptop, with Isabelle installed, to the tutorials.
  • Because there no lectures on the first Monday, we lose the first lecture. To compensate for this, the second lecture starts directly with the technical material. Please read these slides for motivating material.

Material

  • Book: Concrete Semantics including slides and demo theories
  • All IMP theories are in the Isabelle distribution in src/HOL/IMP. You can import theory T like this:
    imports "~~/src/HOL/IMP/T"

Exercises

Homework

Homework is the heart and soul of this course.

  • Solved homework should be uploaded to the submission system, according to the instructions in the first exercise sheet.
  • 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 40% towards the final grade.

Aims

The aim of this course will be 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).
  • 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 or oral 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 (60%) and the homework (40%) grades.
  • All lectures are in English.

Literature