Reading Materials

Reading materials

This is a list of reading materials that I would recommend for any or all of the following reasons:


Introduction to Category Theory

Introduction to Simple Type Theory

Introduction to Haskell

(Not a necessity to learn Agda. Haskell is an incarnation of the kind of theoretical programming languages that is studied in the Formal Systems course.)

Introduction to Dependent Type Theory and Agda

Alternatives are:

Introduction to Coq

(Coq is very powerful but also a bit harder to learn. We usually stick to Agda.)

Introduction to Lean

The Lean theorem prover is newer than both Coq and Agda and has a large community of people working on the formalization of mathematical results.

Homotopy Type Theory (HoTT)

Cubical Type Theory and Cubical Agda


Side effects and Monads

Haskell is a purely functional programming language, meaning that functions behave as in mathematics: they have an input and an output, and the output depends on the input, and that’s it. They do not do anything. Side effects (the technical term for doing something after all) are modelled in Haskell using the category theoretic concept of monads. Relevant resources:

Universal algebra, algebraic theories and its relevance to type theory

Group theory is the study of groups and is an instance of the formal concept of an “algebraic theory / Lawvere theory”.

Simple/dependent type theory can be seen as the study of models of type theory and in this sense is an instance of the formal concept of a “multisorted/generalized algebraic theory”.

Relevant resources:

Presheaf models of type theory

(To the extent that you’re interested. Note: this subject has a tendency to turn your master thesis into a literature study.) For the concept of a model, see the resources on algebraic theories. The idea is that if we have a model of a dependently typed system in which we know that there is no semantic (semantic means: in the model) counterpart of a proof of the false proposition, then our type system must be sound as the false proposition is then known to be unprovable.

The concept of presheaf models is inherently quite technical and takes time to sink in.

Relevant resources:



Good frameworks to typeset your bibliography (assuming you’re using LaTeX) are bibTeX and biber. Both use the same reference file format .bib.

From DBLP you can obtain excellent bibTeX (and other) citation records. Citation records obtained from Google Scholar are often sloppy and need to be manually adjusted where information is missing, wrong, or garbled.

In the 21st century, please make sure that every bibliography entry contains a clickable URL (unless a somewhat permanent-looking link affiliated to either the publisher or one of the authors or their institutions is hard to find).


If you are interested in ongoing research discussions or even job opportunities in the research communities related to our work, the following communication channels may be of interest:

Mailing lists:

Zulip chats:

License: CC BY-NC 4.0