  Understand the basics of complete partial orders (cpo) and domain theory
 Manage the basic machinery for applying domain theory in a computer science context: monotonicity, least upper bound, continuity, least fixed point, Scott induction
 Being able to prove properties about cpos
 Being able to define the denotational semantics of a programming language and of a specific programming construct
 Being able to compute the denotational semantics of a program (in While or in PCF)
 Being able to prove properties about the denotational semantics of a program
 Being able to relate the denotational and the operational semantics of PCF
 Being able to compute the denotational semantics of untyped lambda terms
 Being able to prove properties about the denotational semantics of untyped lambda terms


Semantics of a programming language can be given in an operational, axiomatic and a denotational way. Operational semantics describes the computational behaviour of programs (their evaluation) and axiomatic semantics describes their properties using logical formulas. Denotational semantics describes a program as a mathematical function (basically, a function from input to output). This course studies denotational semantics of programming languages and the mathematical theory required for giving a denotational semantics: domain theory.
We assume that the students are familiar with operational (and preferably also some axiomatic) semantics, especially for a simple imperative "while" language and for a simple functional language like (untyped) lambda calculus. In this course we describe the denotational semantics for the simple imperative programming language "while". Then we move on to PCF, which is the archetypical functional programming language, being a simply typed lambda calculus with two basic data types (booleans and naturals) and a fixedpoint operator. We define the operational semantics of PCF and a notion of program equivalence that emerges from that. program equivalence is given through the important concept of observational (or contextual) equality. We describe the denotational semantics of PCF and we relate the denotational equality with the operational program equivalence.
Mathematically, denotational semantics rests on the field of "domain theory". A domain is an partially ordered structure with some additional properties: they are so called "complete partial orders". The ordering may be regarded as an "information ordering": a larger element contains more information than a smaller element. In the course we study the basic elements of domain theory that are needed to give a denotational semantics to while and PCF: monotonicity and continuity of functions; constructions on domains like the sum, product and function space domain; basic domains like the flat domains of booleans and numbers. We study the important construction of a "least fixed point" of a continuous function and the concept of "Scott induction".
We discuss how different operational semantics (like callbyname and callbyvalue) give rise to a different domain of interpretation. We discuss the notion of sequential computation and show that all the standard domain model for PCF is not "fully abstract". (A notion we will define.) We show how to use domain theory to give a denotational semantics to other formal (programming) languages, especially the untyped lambda calculus. We describe the D_A model as a concrete model for the untyped lambda calculus and study its basic properties, using Bohm trees of untyped lambda term





• Lecture Notes on Denotational Semantics by Andy Pitts and Glynn Winskel. (Available via internet: http://www.cl.cam.ac.uk/~gw104/dens.pdf) • Grondslagen van de Informatica 2 course notes by Erik Barendsen, http://www.cs.ru.nl/~herman/onderwijs/semantics2013/GI2dictaat.pdf • Handout on dI domains: http://www.cs.ru.nl/~herman/onderwijs/semantics2014/didomainsnote.pdf Preknowledge on operational semantics of a simple While programming language (natural semantics or structured operational semantics) is in Hanne Riis Nielson en Flemming Nielson: Semantics with applications, 1999 (available via internet: http://www.daimi.au.dk/~bra8130/Wiley_book/wiley.pdf) 
• 32 hours lecture • 32 hours problem session • 104 hours individual study period Extra information teaching methods: lectures + exercise class 
• complete partial orders (cpos) and domains • monotonicity, continuity, chain, directed set, least upperbound, KnasterTarski fixed point theorem, Scottinduction • operations on domains: product, sum, function space; examples of domains. • denotational semantics of the simple "While" language • program analysis via denotational semantics • the language PCF, functional languages with highertypes; • operational semantics of PCF via callbyname and callbyvalue • denotational semantics of PCF • equivalence of denotational and operational semantics, e.g. via logical relations • full abstraction in PCF • denotational semantics of the untyped lambda calculus • D_A model and Bohm trees 

The following courses taught at the RU give you the required starting knowledge: • beweren en bewijzen • berekenbaarheid • semantiek en correctheid • berekeningsmodellen The required contents of these courses is captured by any set of courses covering
• predicate logic (derivations and models) • operational semantics of a simple While programming language (natural semantics or structured operational semantics) • basic knowledge of lambda calculus Additionally, some knowledge of basic recursion theory would be useful. 
  Required materialsReaderLecture Notes on Denotational Semantics by Andy Pitts and Glynn Winskel. (Available via internet: http://www.cl.cam.ac.uk/~gw104/dens.pdf) 
 ReaderGrondslagen van de Informatica 2 course notes by Erik Barendsen, http://www.cs.ru.nl/~herman/onderwijs/semantics2013/GI2dictaat.pdf 
 HandoutsHandout on dI domains: http://www.cs.ru.nl/~herman/onderwijs/semantics2014/didomainsnote.pdf 

 Recommended materialsBookHanne Riis Nielson en Flemming Nielson: Semantics with applications, 1999 (available via internet: http://www.daimi.au.dk/~bra8130/Wiley_book/wiley.pdf) 

 Instructional modesTestsTentamenTest weight   1 
Opportunities   Block KW4, Block KW4 


 