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
• Peer assessment of Assignment 3
• Introduction to Denotational Semantics
• The meaning of while loops

Class 8 [Chapter 5.2] [Exercises 5.18, 5.21, 5.33, 5.40]

• 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] []

• Introduction to Program Analysis
• Detection-of-signs analysis: introduction

Class 11 [Chapter 7.4] [Exercises 7.28, 7.29]

• Detection-of-signs analysis: definition [rules]
• 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 4
• 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