Course Outline

Below, you find an outline of the course with required reading and recommended exercises, both based on the course book.

Class 1 [Chapter 1.1] [slides]
* Introduction to Semantics for Programming Languages
* Course goals and syllabus
* Course organization and administration
Part I: Operational Semantics and Language Implementation Class 2 [Chapter 1.2-1.4, 2.1] [Exercises 1.13, 2.3, 2.7]
* Syntax of the simple programming language While
* Semantics of arithmetic and boolean expressions
* Inductive definitions and proofs by structural induction
* Natural semantics (aka Big-step operational semantics)
* Description of Assignment 1 (see Assignments)
Class 3 [Chapter 2.2, 2.3] []
* Program termination
* Equivalence between statements [rules]
* Determinism of While
* The semantic function Sns
* Structural operational semantics (aka Small-step operational semantics)
* Configuration graphs and state space exploration [example]
Class 4 [Chapter 3] [Exercise 2.16]
* Peer assessment of Assignment 1
* The semantic function Ssos
* Equivalence of natural and structural operational semantics
* Extending While with additional language features:

* abortion
* non-determinism
* parallelism/concurrency/threads
* subroutines/procedures
* Description of Assignment 2 (see Assignments)
Class 5 [Chapter 4] []
* Correct implementation of programming languages: approach
* An abstract machine: language and semantics
* A translation of While statements into abstract machine code
* Description of Lab Assignment 1 (see Labs)
Class 6 [] [Exercises 4.13, 4.14, 4.19]
* Correctness as semantic equality w.r.t. specification semantics
* Description of Assignment 3 (see Assignments)
* Concluding remarks on operational semantics
Part II: Denotational Semantics and Program Analysis Class 7 [Chapter 5.1] []
* Peer assessment of Assignment 2
* Introduction to Denotational Semantics
* The meaning of while loops
Class 8 [Chapter 5.2] [Exercises 5.18, 5.21, 5.33, 5.40]
* Peer assessment of Assignment 3
* Fixed-point theory
Class 9 [Chapter 5.3, 5.4] [Exercises 5.49, 5.50, 5.51, 5.53]
* Summary of conditions for the Fixed Point Theorem
* Back to the denotational semantics of while loops
* Example: the denotation semantics of while ¬(x=0) do x:=x-2 [example]
* Consistency with the operational semantics of While
* Language properties expressed through denotational semantics:

* determinism
* termination
* equivalence of statements
* Description of Assignment 4 (see Assignments)
Class 10 [Chapter 7.1] []
* Peer assessment of Assignment 4
* Introduction to Program Analysis
* Detection-of-signs analysis: introduction
Class 11 [Chapter 7.4] [Exercises 7.28, 7.29]
* Detection-of-signs analysis: definition
* Detection-of-signs analysis: examples
* Application to program transformation
* Description of Assignment 5 (see Assignments)
Part III: Axiomatic Semantics and Program Verification Class 12 [Chapter 9.2]
* Peer assessment of Assignment 5
* Description of Lab Assignment 2 (see Labs)
* Introduction to Axiomatic Semantics [rules]
Class 13
* Loop invariants
* Proof tableaux: proofs as annotated programs [example-tree] [example-tableau]
* Description of Assignment 6 (see Assignments)
Class 14 [Chapter 9.3]
* Peer assessment of Assignment 6
* Automating program verification

* weakest pre-conditions [notes]
* symbolic execution [notes]
* Soundness and completeness of axiomatic semantics
Class 15
* Course Summary
* Exam Preparation
* Course Evaluation