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

[Ichiro Hasuo]

On Apr 8, 2013 3:59 PM, "Tetsuri Moriya" <tetsuri.moriya at gmail.com> wrote:

> みなさま、
>
> 東京大学の蓮尾研究室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.
>
>
> _______________________________________________
> Logic-ml mailing list
> Logic-ml at fos.kuis.kyoto-u.ac.jp
> http://www.fos.kuis.kyoto-u.ac.jp/cgi-bin/mailman/listinfo/logic-ml
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.fos.kuis.kyoto-u.ac.jp/pipermail/logic-ml/attachments/20130416/1d36c172/attachment.html>