# Category Theory, Monads, and Computation

#### Master level course, 4 ECTS. UR1 / ENS Rennes 2020/21 (sif)

## Syllabus

The main objective of this course is to introduce a different, yet very rich and powerful, point of view to several constructs and structures the students have already seen. After presenting the basics of category theory, we will investigate the concept of monads in both its theoretical roots and practical use in programming languages. We hope that this course serves as an invitation for master students to enrich their toolbox with open-mindedness, elegance and curiosity.

**Keywords**
Category Theory, Monads, Semantics, Functional Programming, Computation, λ-calculus

## Pre-requisite

Licence in mathematics or theoretical computer science or equivalent degree. Functional programming, semantics, programming languages’ theory, logic.

## Roadmap (tentative)

All courses will take place in B02B-E209 – don’t forget your mask!

#### Introduction – Rethinking Set Theory

- September 14 ETCS revisited (1/2)
- September 16 ETCS revisited (2/2)

#### Part 1: Basics of Category Theory [Slides]

- September 21 Categories
- September 23 Functors
- September 28 TD1
- September 30 Natural transformations
- October 5 Adjoints
- October 7 TD2

#### Part 2: Types as Formulas [Slides]

- October 12 Adjoints (Naturality, Unit and Counit)
- October 14 TD3
- October 19 Monads and Kleisli Categories
- October 21 Cartesian Closed Categories (TD4)
- November 2 Deductive systems and λ-calculus (Whiteboard)
- November 4 Curry-Howard-Lambek isomorphism (Whiteboard)

#### Exam

## Evaluation

The final score will be composed of two marks:

- A written exam: November 9, 5 – 7 PM
- All TDs will be marked.

## Seminars

None this year unfortunately.

## Previous Exams

- Exam 2019/2020 [exam]

## Bibliography

- Books
- William Lawvere, Stephen H. Schanuel. Conceptual Mathematics: A First Introduction to Categories. 1997, 2009
- Tom Leinster. Basic Category Theory. 2016 pdf
- Joachim Lambek, Philip J. Scott. Introduction to Higher-Order Categorical Logic. 1986
- Saunders Mac Lane, Categories for the Working Mathematician. 1972

- Papers

## Office Hours

- Thursdays, 2–4 PM (Inria)
- For any request/question, feel free to email me (see address below)