みなさま，

東京大学の蓮尾と申します． 来る12月18日，タリン工科大学の中田景子さんをお迎えしてご講演いただきます． （2題，連続講演です）

詳細は以下です．ご興味のある方はぜひお越しください！

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

-------------------------------------------------------------------------------------------------------------- Tue 18 December 2012, 16:40-18:10 Keiko Nakata (Tallinn University of Technology), 2 titles 理学部7号館1階 102教室 Room 102, School of Science Bldg. No. 7

Title Proving open induction using delimited control operators

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

---

Title Walking through infinite trees with mixed induction and coinduction: A Proof Pearl with the Fan Theorem and Bar Induction.

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