Practical Semantics of Programming Languages

03-05-H-705.56
Category V
Prerequisites: content of 600.01, 600.02, 601.01, 601.02
ECTS: 6
Monday 13:00 - 15:00 MZH 1380 (Kleiner Senatssaal)
Tuesday 13:00 - 15:00 MZH 1380

Start: Tuesday, April 17th

A formal semantics for a given programming language is an important prerequisite for the rigid analysis of the behaviour of its programs, e.g. for purposes of software validation, but also for meta-level issues such as compiler verification. Automatic tool support for such applications hinges on a modeling of the semantics in a suitable proof tool, such as an interactive theorem prover. In this course, we will focus on practical aspects of modelling the semantics of imperative languages in the semiautomatic theorem prover Isabelle.

Literature

• The Isabelle Tutorial
• G. Wynskel: The formal semantics of programming languages, MIT Press, 1993.

Handouts

• Resolution in Isabelle

Exercises

• sheet 1
• sheet 2