[Back to Teaching]
Mathematical Semantics of Computer Systems (AY 2014)
General
- Monday 10.30h-12.00h
- Room 102, School of Science Bldg. No. 7
- For Graduate Students. Code: 4810-1168
- Lectures are in English
Course Objective
Correctness of computer systems and programs is a pressing issue in the modern world. Their verification窶廃roviding mathematical proofs for their correctness窶把alls for the mathematical modeling of systems or programs. This is what the field semantics is all about. And in the modern approaches to program/system semantics, category theory is an indispensable language.
Category theory is used in many different applications; and its use in each application comes with a greatly different flavor. The course exhibits two eminent uses of category theory窶把oncurrency and functional programming窶蚤nd shows two different "faces" of category theory. These different faces are unified in the latter half of the course, where the lectures are led by categorical concepts rather than applications.
Keywords: category theory, algebra, coalgebra, type theory, semantics, reactive system, automaton, functional programming
Course Structure (Tentative)
- Categorical Algebra and Coalgebra
- Introduction to category theory I: the category of sets and functions
- System as coalgebra
- Syntax as an algebraic signature
- Categories and Type Theory
- Introduction to category theory II: cartesian closed categories and more
- The category of types
- Functorial semantics
- Monad
- For branching in coalgebra
- For effect in functional programming
- Presheaf Category
- Further on category theory: the Yoneda lemma
- Binding signature, categorically
Course Material
References
Besides some textbooks and papers mentioned during the lectures, there is a series of fantastic online lectures on category theory by Eugenia Cheng and Simon Willerton. Recommended!
Evaluation
Homework is assigned at the end of each of four parts.
First Report (Due: Mon Nov 26 2012)
- Answer as many exercises as you like, from the course slides, [Mac Lane, Categories for the Working Mathematician], [Awodey, Category Theory], or any other textbooks or papers.
- It is important that you appeal to me you have understood what is told in the lectures.
- Several A4 pages, or a few questions, will be good.
- Deadline: 10:30h, Monday Nov 26 2012.
Second Report (Due: Mon 18 Feb 2013)
- Present the material of your choice to demonstrate what you have got from the lectures. Examples:
- some exercise problems from the latter half of the lecture notes;
- your own review of (part of) the lecture materials (but this has to be a good one);
- a short survey of one of the topics discussed in the lectures, or related ones, such as
- SOS and process algebra
- operational semantics of programming languages
- bialgebra, Hopf algebra, Frobenius algebra, etc. in mathematics or computer science
- the Yoneda lemma
- your paper related to the lectures;
- etc.
The bottom line: show me something interesting.
If you are not sure if your choice of material is suitable, don't hesitate to ask me.
- Several A4 pages will be good.
- Deadline: 12:00h, Monday 18 Feb 2013. Submit it to the lecturer's mailbox, or to the
department report box.
Schedule
- 2012.10.1 (Mon)
- 2012.10.15 (Mon)
- 2012.10.22 (Mon)
- 2012.10.29 (Mon)
- 2012.11.5 (Mon)
- 2012.11.12 (Mon)
- 2012.11.19 (Mon)
- 2012.11.26 (Mon)
- 2012.11.30 (Fri)
- 2012.12.3 (Mon)
- 2012.12.10 (Mon)
- 2012.12.17 (Mon)
-
2013.1.15 (Tue)
(The lecturer is away on a research trip)
-
2013.1.21 (Mon)
(The lecturer is away on a research trip)
- 2013.1.28 (Mon)