皆様
ストックホルム大学のErik Palmgren先生はご都合により来日できないことにな りました。 以下の連続講義を中止いたしますので、ご連絡いたします。
問合せ先： 石原 哉 北陸先端科学技術大学院大学 情報科学研究科 e-mail: ishihara@jaist.ac.jp
On 2015/02/20 11:18, Hajime Ishihara wrote:
皆様
ストックホルム大学のErik Palmgren先生の連続講義のお知らせです。 ふるってご参加ください。
問合せ先： 石原 哉 北陸先端科学技術大学院大学 情報科学研究科 e-mail: ishihara@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.