NWI-IMC011
Semantics and Domain Theory
Course infoSchedule
Course moduleNWI-IMC011
Credits (ECTS)6
CategoryMA (Master)
Language of instructionEnglish
Offered byRadboud University; Faculty of Science; Informatica en Informatiekunde;
Lecturer(s)
Coordinator
prof. dr. J.H. Geuvers
Other course modules lecturer
Lecturer
prof. dr. J.H. Geuvers
Other course modules lecturer
Contactperson for the course
prof. dr. J.H. Geuvers
Other course modules lecturer
Academic year2019
Period
KW1-KW2  (02/09/2019 to 02/02/2020)
Starting block
KW1
Course mode
full-time
Remarks-
Registration using OSIRISYes
Course open to students from other facultiesYes
Pre-registrationNo
Waiting listNo
Placement procedure-
Aims
  • 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
Content
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 fixed-point 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 call-by-name and call-by-value) 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
Level

Presumed foreknowledge
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.
  • Test information
    Written exam.
    Specifics

    Topics
    • complete partial orders (cpos) and domains
    • monotonicity, continuity, chain, directed set, least upperbound, Knaster-Tarski fixed point theorem, Scott-induction
    • 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 higher-types;

    • operational semantics of PCF via call-by-name and call-by-value
    • 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

    Test information
    Written exam.

    Prerequisites
    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 materials
    Reader
    Lecture Notes on Denotational Semantics by Andy Pitts and Glynn Winskel. (Available via internet: http://www.cl.cam.ac.uk/~gw104/dens.pdf)
    Reader
    Grondslagen van de Informatica 2 course notes by Erik Barendsen, http://www.cs.ru.nl/~herman/onderwijs/semantics2013/GI2-dictaat.pdf
    Handouts
    Handout on dI domains: http://www.cs.ru.nl/~herman/onderwijs/semantics2014/didomainsnote.pdf

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

    Instructional modes
    Course occurrence

    Tests
    Exam
    Test weight1
    Test typeExam
    OpportunitiesBlock KW2, Block KW3