みなさま，

念のため，明日の中田景子さんのご講演について 場所と時間の変更のご案内を再度お送りします．

どうかよろしくお願いいたします！ 蓮尾 一郎

---------- Forwarded message ---------- From: Ichiro Hasuo [email protected] Date: Thu, Dec 13, 2012 at 9:06 AM Subject: *** Time & Venue Changed *** Talk by Keiko Nakata (Tallinn U of Tech), Tue 18 December 2012 To: logic-ml [email protected], sonoteno [email protected], [email protected]

みなさま，

こんにちは！ 東京大学の蓮尾と申します． 先日お知らせした，タリン工科大学の中田景子さんによるご講演ですが， ＊＊ 時間と場所を変更 ＊＊ させてください．（日程は同じです） 急なお知らせで申し訳ありません．

また，会場の国立情報学研究所では，中田さんのご講演の前（13:30-15:30）に ToPS セミナーが開催されます．そちらにも是非どうぞ！ http://takeichi.ipl-lab.org/~tops/upcoming_seminar.html

蓮尾 一郎 http://www-mmm.is.s.u-tokyo.ac.jp/

============================================= Tue 18 December 2012, 16:00-17:30 Keiko Nakata (Tallinn University of Technology), 2 Talks 国立情報学研究所 12階 1208号室 Rm. 1208, 12F, National Institute of Informatics Access: http://www.nii.ac.jp/en/about/access

*** 場所・時間が変わりました *** *** The time and venue have been changed *** 中田さんのご講演の前（13:30-15:30）に，同じ場所で ToPS セミナーが開催されます．そちらにも是非どうぞ！http://takeichi.ipl-lab.org/~tops/upcoming_seminar.html Prior to Dr. Nakata’s talk there will be a “ToPS seminar” at the same location. The talks will be of similar research interests. http://takeichi.ipl-lab.org/~tops/upcoming_seminar.html

Talk 1: Proving open induction using delimited control operators Open Induction (OI) is a principle classically equivalent to Dependent Choice, which is, unlike the later, closed under double-negation translation and A-translation. In the context of Constructive Reverse Mathematics, Wim Veldman has shown that, in presence of Markov's Principle, OI on Cantor space is equivalent to Double-negation Shift (DNS). With Danko Ilik, we have reworked Veldman's proof to give a constructive proof of OI, where DNS is interpreted using delimited control operators.

Joint work with Danko Ilik.

Talk 2: Walking through infinite trees with mixed induction and coinduction: A Proof Pearl with the Fan Theorem and Bar Induction. We study temporal properties over infinite binary red-blue trees in the setting of constructive type theory. We consider several familiar path-based properties, typical to linear-time and branching-time temporal logics like LTL and CTL*, and the corresponding tree-based properties, in the spirit of the modal mu-calculus. We conduct a systematic study of the relationships of the path-based and tree-based versions of ``eventually always blueness '' and mixed inductive-coinductive ``almost always blueness'' and arrive at a diagram relating these properties to each other in terms of implications that hold either unconditionally or under specific assumptions (Weak Continuity for Numbers, the Fan Theorem, Lesser Principle of Omniscience, Bar Induction).

Joint work with Marc Bezem and Tarmo Uustalu.