[kisoron-ml] JAIST Logic Seminar Series

[Hajime Ishihara]

皆様

ストックホルム大学のErik Palmgren先生の連続講義のお知らせです。
ふるってご参加ください。

問合せ先：
石原　哉
北陸先端科学技術大学院大学 情報科学研究科
e-mail: ishihara at jaist.ac.jp

--------------------------------------------------
* JAIST Logic Seminar Series *

* This seminar is held as a part of the EU FP7 Marie Curie Actions
IRSES project CORCON (http://corcon.net/).

Date:
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

Place: JAIST, Lecture room I3-I4
(Access: http://www.jaist.ac.jp/english/location/access.html)

Speaker: Professor Erik Palmgren
(Department of Mathematics, Stockholm University)

Title: Lectures on type theory with a view towards formalizing 
Bishop-style mathematics

Abstract:
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.

References

E. Bishop and D.S. Bridges. Constructive Analysis. Springer 1985.
E. Palmgren. Lecture notes on Type Theory. Stockholm 2014.  URL: 
http://kurser.math.su.se/course/view.php?id=48
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.