[logic-ml] Talk by Venanzio Capretta, Thursday next week (Oct 17)

[Ichiro Hasuo]

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.