BeskrivelseCategory theory is an abstract branch of mathematics which has found many applications, in particular in computer science, logic and other fields of mathematics. For computer scientists and logicians, category theory is useful because it provides a set of abstractions useful for organising e.g. denotational models and also a set of tools for constructing new such models. For example, forcing in set theory can be understood via sheaf categories and many concepts in functional programming (e.g. monads) can be described abstractly and studied in category theory. Recently, models constructed using category theory have been used in the design of new type theories, such as homotopy type theory and guarded dependent type theory. In this course we will cover the basic concepts of category theory and illustrate these with applications to denotational semantics of programming languages and logic. The course thus forms a base for further studies of e.g. categorical logic and denotational semantics, such as models of (homotopy or guarded) type theory.
|9 sep. 2016 → 16 dec. 2016