Dear all,

Thursday next week we have Venanzio Capretta from University of Nottingham visiting us in U Tokyo and making a talk on infinite datastructures (related: (co)algebra and (co)induction). No registration needed. See you there!

Best regards, Ichiro Hasuo http://www-mmm.is.s.u-tokyo.ac.jp/

________________________________

Thu 17 October 2013, 17:00-18:00

Venanzio Capretta (U. Nottingham), THE CONSTRUCTION OF INFINITY *理学部7号館2階 214教室* （いつもの1階の部屋ではありません） Room 214, School of Science Bldg. No. 7 (Not the usual one on the ground floor) アクセス： https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html Access: http://www-mmm.is.s.u-tokyo.ac.jp/

This talk is about the implementation and use of infinite data structures in computer science, specifically in constructive type theory. In the first part, I give some history and philosophy of the mathematical theories of infinity, illustrated with some puzzles. The second part is about solving equations on infinite streams: under what conditions does a recursive definition produce a unique function on streams? The third part is about a new kind data type, which I call "Wander Types". It allows the definition of non-well-founded structures with fine control on branching behaviour.