Semantics (2008/2009)

Learning outcomes

The course introduces the main mathematical techniques developed in
the area of "formal semantics of programming languages":

* type systems
* operational semantics
* domain theory
* denotational semantics

1. operational semantics
1.1 definition of a simple imperative language
1.2 evaluation rules

2. induction
2.1 mathematical induction
2.2 structural induction
2.3 well founded induction

3. denotational semantics of a simple imperative language
3.1 a compositional semantics
3.2 the case of while-free programs
3.3 the treatment of the while

4. introduction to domain theory
4.1 complete partial orders
4.2 continuity
4.3 the Knaster-Tarski theorem
4.4 constructions on domains:
products of domains; function domains; flat domains

5 PCF
5.1 Terms and types
5.2 Free variables, bound variables and substitution
5.3 Typing
5.4 Evaluation (operational semantics)

6 Denotational Semantics of PCF
6.1 Denotation of types
6.2 Denotation of terms
6.3 Compositionality
6.4 Soundness

--