Semantics of Programming Languages

Dr. Peter Lammich, Prof. Tobias Nipkow, Wintersemester 2014/15

The course is based on this new book.

• Module: IN2055
• Lectures: Monday 8:30 - 10:00 in MI 00.07.014, Tuesday 8:30 - 10:00 in MI 00.07.014
• Tutorials: Tuesday 10:15 - 11:45 in MI 01.09.014
• Start lectures: 7.10.2014. Start tutorials: 14.10.2014
• Tutors: Peter Lammich

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

News

• We have put on-line the exam of last year, such that you get an impression how a semantics exam looks like. We will not publish sample solutions.
• The written exam
  • You will be allowed to use 2 handwritten or printed A4 sheets of paper, but nothing else.
  • A few questions may be Isabelle-specific, but most of them will deal with semantics.
  • Proofs must be detailed and readable but need not conform exactly to the Isabelle syntax. Major proof steps, especially inductions, need to be stated explicitly. Minor proof steps (corresponding to by simp, by blast etc) need not be justified if you think they are obvious, but you should say which facts they follow from.
  • The questions will all be formal (you need not write an essay) but will not all be proofs but also definitions, calculations etc.
• There will be a tutorial instead of a lecture on Tue, Nov 4, 8:30--10:00 in room MI 00.07.014 (room of the lectures).
• Please bring your laptop, with Isabelle 2014 installed, to the tutorials.
• We use Piazza as a platform for online discussion about the course and the Tutorials.
  Here is the link, you should be able to log in with your TUM-online credentials: https://www.moodle.tum.de/mod/lti/view.php?id=236319 (Note, the link tries to open a pop-up, check your pop-up blocker configuration)
  Please keep your postings abstract enough so that solutions to homework are not easily constructable from them!

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 Exercise 1, Solution, Theory developed in tutorial Exercise 2 (Old version of exercise 2), Solution, Tutorial thy, tmpl02_aexp.thy Exercise 3 tmpl03_ab.thy Solution, Tutorial thy, Exercise 4 Solution, Tutorial thy, Exercise 5, Solution: 1 2, Tutorial thy: 1 2, Template 5.1 Exercise 6, Solution: 1 2 Tutorial: Matches solution 6.1. The proof for IfFalse works (even automatically), if a lemma similar to exec_appendL_if, but for Cons (#) instead of append (@), is added. I also added an Isar-variant of the proof for that case. Exercise 7, Solution: 1 2, Tutorial thy: 1 2, Templates: Repeat_Big_Step.thy, Repeat_Compiler_Template.thy. Exercise 8, Template ex. 8.1 + 8.2 Template hw. 8.1 Int_Less_Induct.thy Solution: 8.1 8.2, Tutorial thy Exercise 9, Solution, Tutorial thy, Exercise 10, Template for 10.1 Solution: 1 2 Tutorial thy: 1 2, Exercise 11, Template ex 11.1 and 11.2 Solution, Exercise 12 Exercise 13

Homework

Homework is the heart and soul of this course.

• Solved homework should be submitted via e-mail to one of the tutors:

  lammichin.tum.de

  Submission Guidelines

  The subject line of the email should contain the string "[Semantics]". Please send a mail with only a single .thy file attached (no archives please). You can always solve all parts of the homework in one theory file! The filename should have the form FirstnameLastname.thy, or FirstnameMiddlenameLastname.thy, or Firstname{Von,Zu,Whatsoever}Lastname.thy (Notice capitalization). This submission format saves us from unpacking and renaming dozens of files manually.

  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.
  Plagirizing 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 combine the grades from the examination (60%) and the homework (40%).
• All lectures are in English.

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.