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.

Outline

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.

Literature

1. Agda and type theory
   • The Agda wiki
   • Dependently Typed Programming in Agda. U.Norell and J. Chapman
   • Chapter 1 of the HoTT book
2. Continuity and the Fan theorem
   • A continuous computational interpretation of type theories. Chuangjie Xu, PhD thesis, 2015.
   • The webpage of Dr. Berger's course on the Fan theorem
3. Analysis
   • Constructive analysis with witnesses. Helmut Schwichtenberg, lecture notes, wintersemester 2016/17, LMU.

Lecture codes and exercises

• 16.10.2017: Introduction I (Agda file, html format). Exercise: Install Agda and run the example in the lecture codes.
• 23.10.2017: Introduction II (unfilled lecture codes, lecture codes, html format). Exercise: Prove the 5 logical axioms left in the lecture codes.
• 30.10.2017: Arithmetic (unfilled lecture codes, lecture codes, html format). Exercise: Prove the 4 properties of multiplications left in the lecture codes.
• 06.11.2017: Continuity in Type Theory I (slides, informal proof, unfilled lecture codes, lecture codes).
• 13.11.2017: Continuity in Type Theory II (slides, unfilled lecture codes, lecture codes, html format). Exercise: Complete the logic of propositions.
• 20&27.11.2017: Uniform Continuity in Type theory (slides, unfilled lecture codes, lecture codes, html format).
• 04&11&18.12.2017: The Fan Theorem (lecture codes, html format)

Chuangjie Xu

Last modified: Thur 28th Dec 2017