Introduction to Type Theory (OPLSS 22)

Type Theory is at the same time an alternative to set theory as a mathematical foundation and a programming language originally conceived by the Swedish philosopher and mathematician Per Martin-Löf. The course is an introduction to Type Theory which covers the following topics:

(Simpy typed) λ-calculus and combinatory logic
Propositions as types
Classical vs intuitionistic reasoning
Dependent types, Π- and Σ-types
Reasoning in Type Theory, Equality
Inductive and coinductive types
Universes and paradoxes

Chapters from my forthcoming book (The Tao of Types) will be made available to the participants.

Agda

We are using the agda system : an implementation of a dependently typed programming language with a sophisticated GUI.

Installation instructions are available on the agda wiki.

Installing via cabal (the Haskell packet manager) you need install the Haskell platform first. You will also need emacs (or atom) to be installed on your machine.

The standard library has to be installed separately. The instructions are here.

Alternatives: There is a windows installer but I haven't tried it and I don't think it installs the standard library.

Another alternative (avoiding installation altogether) is to use agdapad: this gives you an editor in the browser and connects to an agda server. However, this is unsuitable for bigger projects and I don't know wether we can rely on this.

Lecture notes (chapters of Tao of Types):

Material from the lectures:

Monday (intro, functions): agda file
Tuesday (products & sums, propositions as types): agda file
Wednesday (classical principles, inductive and coinductive types): agda file
Thursday (dependent types, eliminators and coinduction): agda file
Friday (Homotopy Type Theory, cubical agda): agda file, agda file (cubical)

Exercises:

Monday
Tuesday , you need mylib.agda
Wednesday , I have updated mylib.agda
Thursday , I have updated mylib.agda
Friday , Friday (cubical)

Last modified: Fri Jun 24 15:25:41 PDT 2022 Friday