Semantic Methods

10 credits

Syllabus, Master's level, 1MA057

This course has been discontinued.

A revised version of the syllabus is available.

Code: 1MA057
Education cycle: Second cycle
Main field(s) of study and in-depth level: Mathematics A1N
Grading system: Fail (U), Pass (3), Pass with credit (4), Pass with distinction (5)
Finalised by: The Faculty Board of Science and Technology, 6 November 2007
Responsible department: Department of Mathematics

Entry requirements

120 credit points and 90 credit points Mathematics and Computer Science

Learning outcomes

In order to pass the course (grade 3) the student should

master lattice theoretical concepts:

be able to describe various fixed point theorems and their relation to recursive procedures;

be able to describe various categories of domains and give an account of common domain constructions such as function space, product, and sum within various categories;

know and understand the interpretation of simple typed lambda calculus in Cartesian closed categories;

understand the intuitive connection between computability and continuity;

be able to reason in an abstract category with concepts such as product, exponent and monads;

have an understanding of data structures as solutions of domain equations or as initial or final algebras;

be acquainted with fundamental aspects of game semantics;

be able to solve domain equations and to give a model for untyped lambda calculus;

be acquainted with semantics for linear logic;

be acquainted with quantum computation formalism.

Content

Fixed points. Various domain concepts: cpo, algebraic cpo, Scott–Ershov domains. Domain constructions, domain equations and the theory for their solutions. Briefly about topological concepts related to domain theory. Alternative ways to present domains: neighbourhood systems, information systems. Briefly about computable domains, power domains, universal domains and formal topological spaces.

Category theoretical concepts: Adjoints, initial and final algebras, monads, monoidal categories and functor categories.

Models of lambda calculus. Game semantics and models of linear logic. Semantics for quantum programming languages.

Instruction

Lectures and problem solving sessions.

Assessment

Written and, possibly, oral examination at the end of the course. Moreover, compulsory assignments may be given during the course.