This course aims at giving you a solid introduction to category theory, and to apply concepts from category theory to gain insights in some advanced notions within functional programming.

This is a 2 ECTS Ph.D. course within the Computer Science and Engineering programme at the Doctoral School of Technology and Science at Aalborg University.

Through this course you will gain insight in the basic concepts of category theory, an organizing paradigm increasingly used in many areas of computer science and mathematics. This will hopefully help you to be more structured in your research and to avoid pitfalls. You will also gain an understanding of modern functional programming and its relations to other fields.

The course will take place on the following four days in October 2009, each day from 9:00 to 15:00:

- Thursday 1 October
- Wednesday 7 October
- Wednesday 21 October
- Wednesday 28 October

The course will subsume four kinds of activity: lectures and exercises in category theory, and lectures and exercises in functional programming. In the beginning we will do more category theory, and in the end the functional programming part will have more weight.

Lectures and exercises in category theory will be given and supervised by Uli Fahrenberg; those in functional programming by Rene R. Hansen.

In order to pass the course, we will require you to present the solution of a selected exercise to the other course participants. More details on this during the first lecture.

Category theory:

- Categories, duality, functors
- Natural transformations, adjunctions
- Universality, limits, co-limits
- Monads, algebras, co-monads, co-algebras
- Examples, examples, examples; from computer science and mathematics

Functional programming:

- Introduction to Haskell
- Advanced constructions in Haskell
- Monads in functional programming

For the **category theory part** of the course, we will use the following as a basic textbook:

- Benjamin C. Pierce: Basic category theory for computer scientists. MIT Press, 1991

- David E. Rydeheard, Rod M. Burstall: Computational category theory. Prentice Hall, 1988. Available at http://www.cs.man.ac.uk/~david/categories/book/
- Saunders Mac Lane: Categories for the working mathematician. Springer, 1998

For the **functional programming part** of the course, we will mainly use the following:

- Bryan O'Sullivan, John Goerzen, Don Stewart: Real World Haskell. O'Reilly, 2008. Available at http://book.realworldhaskell.org/

We will additionally make use of the following sources:

- Glynn Winskel, Mogens Nielsen:
*Models for Concurrency.*In S. Abramsky, Dov M. Gabbay, and T.S.E. Maibaum: Handbook of Logic in Computer Science, vol. 4. Oxford University Press, 1995. Also available at http://www.daimi.au.dk/PB/463/PB-463.pdf - Michael B. Smyth, Gordon D. Plotkin:
*The Category-Theoretic Solution of Recursive Domain Equations.*SIAM Journal of Computing 11(4):761-783 (1982). Available at http://homepages.inf.ed.ac.uk/gdp/publications/Category_Theoretic_Solution.pdf - Mads Rosendahl:
*Introduktion til domæneteori*(Danish). DIKU 1995. Available at http://akira.ruc.dk/~madsr/webpub/domaene.pdf

Below follows a list of topics and material which can guide you further in exploring the land of categories and functional programming:

**Cartesian closed categories.**These are a special kind of categories which are important for applications in computer science. They are covered in*Pierce*Section 3.1 and*Mac Lane*Section 4.6.- Closely related is the more advanced notion of
**monoidal categories**, which are categories with an extra "tensor" product. These are covered in*Mac Lane*Chapter 7; especially interesting for computer scientists is*Mac Lane*Section 7.7. **Galois connections**are a concept heavily used in static analysis, especially abstract interpretation. Essentially these are adjoint functors between preorder categories. They are introduced in*Mac Lane*Section 4.5.- Following up on
*Winskel-Nielsen*'s important work on the category of transition systems, the notion of**open maps**gives a categorical characterization of*bisimulation*. The standard reference on this is - Categorical formalisms and bisimulation-via-open-maps are useful for relating different formalisms. For
*timed automata*for example, there is a notion of open maps in- Mogens Nielsen, Thomas Hune:
*Bisimulation and Open Maps for Timed Transition Systems.*Fundamenta Informaticae 38(1-2):61-77 (1999). Available at http://www.brics.dk/RS/98/4/index.html.

- Mogens Nielsen, Thomas Hune:
- The notion of
**co-monads and co-algebras**, dual to the one of monads and algebras, gives a different view on formal models. Essentially, a given formal model can be seen as a co-algebra for some functor, and bisimulation can be explained via*co-induction*to the*final co-algebra*. The standard reference is- Jan Rutten:
*Universal coalgebra: A theory of systems.*Theoretical Computer Science 249(1):3-80 (2000). Also available at http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.34.1958.

- Jan Rutten: