Semantics of Programming Languages

Time and Location

• Tuesdays, 15:00 - 16:30, in MI 01.11.018 ("Konrad Zuse")
• Wednesdays, 16:00 - 17:30, in MI 01.11.018 ("Konrad Zuse")

Slides and Lecture Material

• [lec01.pdf] [lec01.ps.gz] [lec01-print.ps.gz] [Hw01.thy]
  
• [lec02.pdf] [lec02.ps.gz] [Lec02.thy]
• [lec03.pdf] [lec03.ps.gz] [Lec03.thy] [Hw03.thy] [Hw03_sol.thy]
• [lec04.pdf] [lec04.ps.gz] [Lec04.thy]
• [lec05.pdf] [lec05.ps.gz] [Lec05a.thy] [Lec05b.thy] [Hw05.thy] [Hw05_sol.thy]
• [lec06.pdf] [Lec06.thy]
• [lec07.pdf] [Lec07.thy] [Hw07.thy] [Hw07_sol.thy]
• [lec08.pdf] [Lec08.thy] [Hw08.thy] [Hw08_sol.thy]
• [lec09.pdf] [Lec09.thy]
• [lec10.pdf] [Lec10.thy] [Hw10.thy] [Hw10_sol.thy]
• [lec11.pdf] [Lec11.thy]
• [lec12.pdf] [Lec12.thy]
• [lec13.pdf] [Lec13.thy] [Hw13.thy] [Hw13_sol.thy]
• [lec14.pdf] [Lec14.thy]
• [lec15.pdf] [Lec15.thy]
• [lec16.pdf] [Lec16.thy] [lec16a.thy] [Lec16b.thy] [Hw16.thy] [Hw16_sol.thy] [Nominal.tgz]
• [lec17.pdf] [Lec17.thy]
• [lec18.pdf] [Lec18.thy]
• 2 guest lectures by Dr Stefan Berghofer [lec19.pdf] [Lec19.thy] [nominal_inductive.ML]
• [lec21.pdf]
• [lec22.pdf] [Lec22.thy]
• [lec23.pdf] [Lec23.thy]
• [lec24.pdf]

Aims

At the end of the course students should

• be familiar with rule-based presentations of the operational semantics of some simple imperative, functional and interactive program constructs
• be able to prove properties of an operational semantics using various forms of induction (mathematical, structural, and rule-based) and
• be familiar with the theorem prover Isabelle

Recommended Books

• Pierce (2002). Types and Programming Languages. MIT Press.
• Gunter (1992). Semantics of Programming Languages. MIT Press.
• Nipkow, Paulson and Wenzel (2007). Tutorial on Isabelle. Springer.

To obtain the ECTS credit points assigned to this course, you have to

• be present in all lectures,
• actively participate in discussions,
• solve all exercises in Isabelle and
• sit an end-of-term exam

Similar courses exist at

• UPenn
• Cambridge
• Harvard