[Back to Teaching]

Mathematical Semantics of Computer Systems (AY 2016)

General

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

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

Course Material

Coming soon

Evaluation

Based on homework assignments.

Schedule