[logic-ml] 4/16, Talk by Keisuke Nakano (Univ. Electro-Communications)

[Tetsuri Moriya]

みなさま、

東京大学の蓮尾研究室M2の森谷です。
蓮尾研究室では4月16日に電気通信大学の中野圭介さんをお迎えしてご講演いただきます。

詳細は以下で、事前の登録等は一切不要です。ご興味のある方はぜひお越しください！

=============================================================
Tue 16 April 2013, 15:30-17:30
Keisuke Nakano (Univ. Electro-Communications), 2 Talks
理学部7号館1階 102教室   Room 102, School of Science Bldg. No. 7

Talk 1: Juggling meets coinduction
In this talk, I will present an application of coinduction, juggling.
 Buhler et al. presented a mathematical theory of toss juggling by
regarding a toss pattern as an arithmetic function, where the function must
satisfy a condition for the pattern to be valid.  In this talk, I will
formalize their theory in terms of coinduction, reflecting the fact that
the validity of toss juggling is related to a property of infinite
phenomena.  A tactic is implemented for proving the validity of toss
patterns in Coq.  Additionally, the completeness and soundness of a
well-known algorithm for checking the validity is certified.  The result
exposes a practical aspect of coinductive proofs.  Most part of this talk
has been presented in CPP 2012.  Some open problems also will be introduced.

Talk 2: Metamorphism in jigsaw
In this talk, I will present a new computation model for metamorphism.  A
metamorphism is an unfold after a fold, consuming an input by the fold then
generating an output by the unfold.  It is typically useful for converting
data representations, e.g., radix conversion of numbers.  Bird and Gibbons
have shown that metamorphisms can be incrementally processed in streaming
style when a certain condition holds because part of the output can be
determined before the whole input is given.  However, whereas radix
conversion of fractions is amenable to streaming, radix conversion of
natural numbers cannot satisfy the condition because it is impossible to
determine part of the output before the whole input is completed. In this
talk, I present a jigsaw model in which metamorphisms can be partially
processed for outputs even when the streaming condition does not hold.  The
jigsaw model allows us to process metamorphisms in a flexible way that
includes parallel computation.  We also apply our model to other examples
of metamorphisms.  Most part of this talk is recently published in Journal
of Functional Programming.  Additionally, I will present some further work
on this work.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.fos.kuis.kyoto-u.ac.jp/pipermail/logic-ml/attachments/20130408/7ebce005/attachment.html>