In the JAIST Logic Seminar Series, Professor Erik Palmgren (Department of Mathematics, Stockholm University) will give a series of lectures:
Lectures on type theory with a view towards formalizing Bishop-style mathematics
In this series of three lectures we give an introduction to Martin-Lof type theory and the tools it provides for formalizing Bishop-style constructive mathematics.
The first lecture will cover basic principles of type theory and give an introduction to its manifestation in the well-known proof assistant Coq.
In the second lecture we consider “Bishop’s set theory” (Bishop and Bridges 1985) from the point of view of type theory, which will involve a development the theory of setoids and subsetoids.
The third lecture will cover models constructive set theory (CZF) in type theory, and how it can be used to solve the problem of universes of setoids and development of category theory.
Throughout the lectures we provide examples and suggestions how you can yourself experiment with the Coq system in the formalization of constructive mathematics.
E. Bishop and D.S. Bridges. Constructive Analysis. Springer 1985.
E. Palmgren. Lecture notes on Type Theory. Stockholm 2014.
E. Palmgren and O. Wilander. Constructing categories and setoids of setoids in type theory. Logical Methods in Computer Science. 10(2014), Issue 3, paper 25.
Lecture 1. Monday 9 March, 2015, 15:10-16:40
Lecture 2. Tuesday 10 March, 2015, 15:10-16:40
Lecture 3. Wednesday 11 March, 2015, 15:10-16:40
All the lectures will take place at JAIST, Lecture room I3-I4