Executing Proogs as Computer Programs

Monday 14-16, HS B 252, start 16th October 2017

The objective is to encourage students to make use of proof assistants in their study of mathematics. I use Agda for demonstration.


  1. Introduction
    1. Computer assisted formalisation of mathematics
    2. Martin-Löf type theory & "Proofs as Programs"
    3. Introduction to the Agda proof assistant
  2. Continuity in type theory
    I will present some results about continuity from my PhD thesis to show
    1. the subtle problem of expressing "existence" in type theory, and
    2. how to make axioms computational.
  3. The Fan theorem
    Dr. Josef Berger is lecturing a course on the Fan theorem (Wednesday 14-16, B040). I'd like to invite students to attend his lectures and formalise some results of the Fan theorem in Agda.
  4. Real numbers
    The last part of the course is to develop a basic fragment of the theory of real numbers in Agda, following the method of Prof. Helmut Schwichtenberg in his previous course on constructive analysis.


  1. Agda and type theory
  2. Continuity and the Fan theorem
  3. Analysis

Lecture codes and exercises

Chuangjie Xu

Last modified: Mon 20th Nov 2017