POPL2013楽しそうだのう。
住井さんが実況してたCopatternsの話がなんだか面白そう。
萩野先生(+Tatsuya Hagino)の Symmetric ML の名前が出てきてたことによる興味というのもあるけれど(Symmetric ML 懐かしいなぁ)。
https://twitter.com/esumii/status/294035025396117504
https://twitter.com/esumii/status/294036168184573952
https://twitter.com/esumii/status/294037122162233345
観測結果を書くことによる定義は、今なら単純なパターンに対してだけでなく複雑なパターンに対してもFutumorphismあたりへdesugarする形で綺麗に扱えそう。もちろん、そんなだけの話ではないのだろうけれど。
あと、この著者陣からすると、Agda で帰納的な定義と余帰納的な定義が混在したときのややこしい問題とかが、綺麗に扱えるようになっていたら、嬉しいなぁ。
Copatterns: programming infinite structures by observations
http://dl.acm.org/citation.cfm?doid=2429069.2429075
http://www2.tcs.ifi.lmu.de/~abel/popl13.pdf