Institute of Information Science, Academia Sinica

This tutorial starts with briefly introducing the category theory through fundamental theorems (Yoneda lemma and Freyd adjoint functor theorem) as well as through an essential notion (monads).

A relationship to logic is given between Cartesian closed category and typed lambda-calculus so that the category theory gives a mathematical substance to Curry-Howard isomorphism.

Further investigation is given in terms of elementary toposes and their logic (e.g., Kripke-Joyal definition of truth). In more concrete aspects, we model Gentzen style cut-elimination for proofs, --statically by denotational semantics and --dynamically by feedback in traced monoidal categories.