Formal semantics of programming languages PDF

Slides and Files Slides (21.1.: p. 442)

Exercises

If you use the Mercurial version control system, you can synchronize these files automatically: hg clone https://www4.in.tum.de/~krauss/hg/semantics_website
[ view changelog ]

Homework

Homework is the heart and soul of this course.

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

  boehmesin.tum.de or kraussin.tum.de

  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 two, one or zero points, depending on the solution being correct, improvable or incorrect, respectively.
• 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. Cheating on one homework will result in zero points for that homework. If you cheat repeatedly, you will fail the course immediately. This applies for both parties, that is, the one who cheated and the one who provided his/her solution.
• Important: homeworks are graded and have a 40% share on 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 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.