Semantic Methods

10 credits

Syllabus, Master's level, 1MA057

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, 30 August 2018
Responsible department
Department of Mathematics

Entry requirements

120 credits and 90 credits in mathematics and Computer Science. Proficiency in English equivalent to the Swedish upper secondary course English 6.

Learning outcomes

On completion of the course, the student should be able to:

  • use lattice theoretical concepts:
  • describe various fixed point theorems and their relation to recursive procedures;
  • describe various categories of domains and give an account of common domain constructions such as function space, product, and sum within various categories;
  • give an account of the interpretation of simple typed lambda calculus in Cartesian closed categories;
  • give an account of the connection between computability and continuity;
  • reason in an abstract category with concepts such as product, exponent and monads;
  • give an account of data structures as solutions of domain equations or as initial or final algebras;
  • solve domain equations and to give a model for untyped lambda calculus;
  • give an account of PCF and the relation between its operational and denotational semantics.

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. Operational and denotational semantics of PCF. Optionally, some elements about game semantics. Semantics for quantum programming languages.

Instruction

Lectures and problem solving sessions.

Assessment

Written at the end of the course combined with assignments given during the course.

If there are special reasons for doing so, an examiner may make an exception from the method of assessment indicated and allow a student to be assessed by another method. An example of special reasons might be a certificate regarding special pedagogical support from the disability coordinator of the university.

FOLLOW UPPSALA UNIVERSITY ON

facebook
instagram
twitter
youtube
linkedin