[kisoron-ml] JAIST Logic Seminar Series

[Hajime Ishihara]

皆様

ルートヴィヒ・マクシミリアン大学ミュンヘンのChuangjie 
Xu博士の講演のお知らせです。
どうぞふるってご参加ください。

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

* JAIST Logic Seminar Series *

* The seminar below is held as a part of JSPS Core-to-Core Program,
A. Advanced Research Networks, and EU FP7 Marie Curie Actions IRSES 
project CORCON.
(http://www.jaist.ac.jp/logic/ja/core2core, https://corcon.net/)

Date: Wednesday 28 September, 2016, 15:20-17:00

Place: JAIST, Collaboration room 7 (I-56)
(Access: http://www.jaist.ac.jp/english/location/access.html)

Speaker: Chuangjie Xu (Ludwig-Maximilians-Universität München)

Title: Continuity in Type Theory

Abstract:
   If all functions (N -> N) -> N are continuous then 0 = 1. We
   establish this in intuitionistic type theory, with existence in the
   formulation of continuity expressed as a Sigma-type via the
   Curry-Howard interpretation.  But with an intuitionistic notion of
   anonymous existence, defined as the propositional truncation of
   Sigma, it is consistent that all such functions are continuous. On
   the other hand, any of these two intuitionistic conceptions of
   existence give the same, consistent, notion of uniform continuity
   for functions (N -> 2) -> N.  Moreover, we constructively develop a
   model of uniform continuity and implemented it within type theory
   using Agda.