    Course module   NWIIMC011  Category   MA (Master)  Language of instruction   English  Offered by   Radboud University; Faculty of Science; Informatica en Informatiekunde;  Lecturer(s)     Academic year   2019   Period   KW1KW2  (02/09/2019 to 02/02/2020) 
 Starting block   KW1  
 Course mode   fulltime  
 Remarks     Registration using OSIRIS   Yes  Course open to students from other faculties   Yes  Preregistration   No  Waiting list   No  Placement procedure    
       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


  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. 
  


• 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 modesTestsExamTest weight   1 
Test type   Exam 
Opportunities   Block KW2, Block KW3 


  
 
 