[Back to Teaching]

Mathematical Semantics of Computer Systems (AY 2016)

General

• Monday 10.25 - 12.10
• Room 102, School of Science Bldg. No. 7 (map)
• 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—providing mathematical proofs for their correctness—calls for their mathematical modeling; this is what the field called semantics is all about. The course introduces some basic techniques in the field, most notably those which employ category theory.

Keywords: category theory, lambda calculus, type theory, logic, categorical semantics, algebraic semantics, denotational semantics, algebra, coalgebra, automaton, fibration, categorical logic

References

• [Lambek & Scott 1986]
J. Lambek, P. J. Scott, Introduction to Higher-Order Categorical Logic. Cambridge University Press, 1988
• [Awodey 2010]
S. Awodey, Category Theory. Oxford University Press, 2010.
• [Leinster 2014]
T. Leinster, Basic Category Theory. Cambridge University Press, 2016.
• [Jacobs 2012]
Bart Jacobs, Introduction to Coalgebra: Towards Mathematics of States and Observations. Draft of a book, available online. 2012
• [Jacobs, 1999]
Bart Jacobs, Categorical Logic and Type Theory. Elsevier Science, 1999

Besides the above ones, there is a series of fantastic online lectures on category theory by Eugenia Cheng and Simon Willerton. Recommended!

Course Structure (Tentative)

1. Basic Category Theory

We exhibit basic constructs in category theory used in the subsequent parts.

• categories, functors, natural transformations
• monoids and preorders as degenerate cases
• epis and monos
• (co)products, (co)equalizers, (co)limits
• adjoint functors, equivalences of categories
• exponents, Cartesian closed categories

We will roughly follow [Lambek & Scott 1986, Part 0] which is however way too fast for beginners; [Awodey 2010, Leinster 2016] will be nice supplementary material.

Goal of Part I: familiarize yourself with the Yoneda lemma, a celebrated result in category theory by Prof. Nobuo Yoneda (Dept. IS, U. Tokyo), desirably in its end/coend form.

2. The Curry-Howard-Lambek Correspondence

As a first example of categorical semantics, a correspondence between typed lambda-calculi and Cartesian closed categories is introduced. An emphasis is on the view that categorical semantics is an extension of algebraic semantics (such as Boolean algebras for classical logic and Heyting algebras for intuitionistic logic).

• typed lambda-calculi
• natural deduction for intuitionistic logic
• syntactic presentation of Cartesian closed categories
• free Cartesian closed categories and completeness

We will follow [Lambek & Scott 1986, Part 1] omitting some topics.

Goal of Part II: the completeness result for Moggi's computational lambda-calculus as an extension of the Curry-Howard-Lambek correspondence, following

Computational lambda-calculus and monads. Tech. Report ECS-LFCS-88-66, Edinburgh Univ., 1988. [pdf]

3. Coalgebras and State-Based Transition Systems

Our second usage of category theory has quite different a flavor: it models various state-based transition systems as coalgebras, a categorical dual of algebras. Here the view of categories as "many-sorted algebras (or monoids)" is not so important as in the previous part---in fact we will almost exclusively work in the category of sets and functions. An alternative categorical genericity from which we benefit is a functor as a parameter: it allows to develop a uniform theory of state-based systems like automata of various kinds (deterministic, nondeterministic, probabilistic, or even quantum).

• coalgebraic modeling
• bisimulation
• final coalgebras
• (process algebra and bialgebra)

We will follow [Jacobs 2012, Chapters 1-3].

Goal of Part III: Familiarize yourself with \emph{coinduction as a proof principle}. Prove some stream equalities with the principle.

4. Fibrations and Categorical Logic

The last part introduces a more advanced bit of category theory, namely the theory of fibrations that are a categorical way of "organizing indexed entities." It will be applied to modeling predicate logic, extending Part 2. If time allows another application, namely coinductive predicates in state-based transition systems, will be introduced. This will unify the views in Parts 2--3 and illustrate the versatility of the mathematical language of category theory.

• fibrations
• indexed categories, the Grothendieck construction
• fiberwise structures
• (co)products between fibers
• equational logics as fibrations
• first-order predicate logics as fibrations
• (inductive and coinductive predicates)

The topics are picked from [Jacobs, 1999]

Goal of Part IV: Understand coinduction up-to formulated in a fibration, as in

Filippo Bonchi, Daniela Petrisan, Damien Pous, Jurriaan Rot: Coinduction up-to in a fibrational setting. CSL-LICS 2016: 20

Coming soon

Evaluation

Based on homework assignments.

Schedule

• 2016.9.26 (Mon) Introduction to the course. Started with the definition of category, with Sets as the first example. In the next lecture we will start with further examples. We had 30+ audience :)
handout, notes
• 2016.10.3 (Mon) We had even more attendants :) Went slowly, through first examples of categories (preorders, monoids and the category of monoids), and the definition of product. handout notes
• 2016.10.17 (Mon) Products, coproducts, universality, monos, epis, isomorphisms. handout notes report solution
• 2016.10.24 (Mon) Functors, natural transformations, Galois connections, and the (equational) definition of adjunction. handout notes
• 2016.10.31 (Mon) Adjunctions: definition, examples, characterization by a natural isomorphism between homfunctors. handout notes
Report assignment: answer the questions 1a, 1b, 2a, 2b in the notes found at this link. Part of the answers are there; you need to fill in the details and complete the proofs. Your report is due at the beginning of the next lecture (Mon 7 Nov). Report Answer
• 2016.11.7 (Mon) Further on adjunctions; limits and colimits. In the next lecture we will start with formal definitions of (co)limit. The report assignments in the original handout have been canceled. handout notes
• 2016.11.14 (Mon) Definitions of (co)cone, (co)limit; the construction of (co)limits via (co)products and (co)equalizers; and how they translate in the category Sets. Next: adjunction and limits.
handout notes
• 2016.11.21 (Mon) Limits and colimits as adjoints; intro. to the Yoneda lemma; full and faithful functors. There is a report assignment.
handout
notes