[kisoron-ml] JAIST Logic Seminar Series

[Hajime Ishihara]

皆様

ストックホルム大学のErik Palmgren先生はご都合により来日できないことにな 
りました。
以下の連続講義を中止いたしますので、ご連絡いたします。

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


On 2015/02/20 11:18, Hajime Ishihara wrote:
> 皆様
>
> ストックホルム大学の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.
>