Topic outline
 
Formal Semantics of Programming Languages (326.027, WS 2006/07)

Time:
Friday, 10:15-11:45.
Room:
HS 11.
Start:
October 6, 2006.

While the syntax of a programming language is always formally specified, the equally important aspect of definining its meaning is often left to natural language which is ambiguous and leaves many questions open. In order to understand the inherent properties of a language (e.g. for constructing a compiler), we should have a deeper understanding.

This course presents some major methods for defining the meaning of programming languages (and thus programs) and discusses their relationship:

Denotational Semantics
A programming language is defined by a valuation function that maps a program into a mathematical object which is considered as its meaning.
Operational Semantics
A programming language is defined by reduction rules that describe how the initial state of a program is transformed step by step into the terminal state.
Axiomatic Semantics
A programming language is defined by correctness assertions that describe how to draw conclusions about the input/output interface of a program.
The participants are expected to elaborate small exercises which will be used for grading (there will be no final exam).
To take part in the course, you have to enrol in the KUSSS system. If you also login in Moodle and register as a course participant, you will receive per email all messages posted in the News forum.

Forum News forum
Resource Syllabus
Resource Literature
Resource The Java Language Specification
 
1
Denotational Semantics (Part 1)
Resource Denotational Semantics
Resource Syntax
Resource Figures (protected)
Resource Sets, Functions, Domains
Resource Semantic Algebras
Resource Basic Structure of Denotational Definitions
Resource Figures (protected)
Resource Imperative Languages 1
Resource Figures (protected)

2
Operational Semantics 
Resource Introduction (protected)
Resource Equivalence with Denotational Semantics (protected)

3
Denotational Semantics (Part 2)
Resource Domain Theory 1
Resource DomainTheory 2 (protected)
Resource Imperative Languages 2
Resource Figures (protected)

4
Languages with Contexts
Resource Languages with Contexts 1: A Block-Structured Language
Resource Figures (protected)
Resource Languages with Contexts 2: An Applicative Language
Resource Figures (protected)
Resource Languages with Contexts 3: Compound Data Structures

5
Axiomatic Semantics
Resource Axiomatic Semantics (protected)

6
Exercises