[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: 48101168
 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 HigherOrder 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)
 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.

The CurryHowardLambek Correspondence
As a first example of categorical semantics, a correspondence
between typed lambdacalculi 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 lambdacalculi
 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 lambdacalculus
as an extension of the CurryHowardLambek correspondence, following
Computational lambdacalculus and monads. Tech. Report ECSLFCS8866, Edinburgh Univ., 1988. [pdf]

Coalgebras and StateBased Transition Systems
Our second usage of category theory has quite different a flavor:
it models various statebased transition systems as coalgebras, a
categorical dual of algebras. Here the view of categories as
"manysorted algebras (or monoids)" is not so important as in the
previous partin 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 statebased 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 13].
Goal of Part III:
Familiarize yourself with \emph{coinduction as a proof
principle}. Prove some stream equalities with the principle.

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 statebased
transition systems, will be introduced. This will unify the views
in Parts 23 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
 firstorder predicate logics as fibrations
 (inductive and coinductive predicates)
The topics are picked from [Jacobs, 1999]
Goal of Part IV: Understand coinduction upto formulated in a fibration,
as in
Filippo Bonchi, Daniela Petrisan, Damien Pous, Jurriaan Rot: Coinduction upto in a fibrational setting. CSLLICS 2016: 20
Course Material
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
report answer
 2016.11.28 (Mon)
(Canceled due to the lecturer's sudden severe fever... my apologies)
 2016.12.5 (Mon)
Finished the part on the Yoneda lemma (sketching its (co)end presentations). Started introduction to algebraic semantics, with the question "how do we prove absence of a proof tree?".
handout
notes
 2016.12.12 (Mon)
Finished algebraic semantics, and untyped lambdacalculus (syntax, betaconversion). In the next lecture we're gonna start with the syntax of simply typed lambdacalculus.
handout
notes
 2016.12.19 (Mon)
Typed lambdacalculus, its categorical semantics (types as objects, terms as arrows), introduction to exponentials. Next: formal definition of exponentials.
handout
notes (available only from the UTokyo network)
 2017.1.9 (Mon) (Public holiday, no lecture)
 2017.1.16 (Mon)
Exponentials, the adjunction induced by them, and recap of the typed lambdacalculus. Next: soundness of CCCs and coalgebra.
handout
notes
 2017.1.23 (Mon)
Finished the categorical semantics of typed lambdacalculus.
handout
(There was a mistake in the handout: in the equation (2) evens should be odds. It's corrected now)
notes
 2017.1.30 (Mon)
On coalgebras and categorical modeling of statebased dynamics.
handout
(There was a mistake in the handout: in the equation (2) evens should be odds. It's corrected now)
notes