Leightweight Language Future (LLFuture) と、等価変換セミナーに行ってきた。

LL Future

LL Futureでは、id:sumiiさんがラムダ式や、ユークリッドのアルゴリズムなどの歴史を語っていたのがおもしろかった。数学でのおもしろい概念は何百年後も利用されるのか。
じゃあ今、数学(や計算機科学)でホットな話題が100年後利用されるのかな？学術分野で今ホットなことってなんだろう？

今回のイベントは未来のプログラミングがテーマなのに、全体的にプログラムの品質などについて言及している人が少なかった気がする。ちょっと不思議だと思った。

ともあれ、控え室などでいろんな人とお話出来たのはなによりの収穫だった。

• Haskellのshelarcyさんとラムダな話ができた。未来のHaskellには依存型が入るとか、System Fが入るとか。
• Haskellのid:nobsunさんと名刺交換できた。nobsunのソースコードから、厳格な厳しい感じの人を想像していたが、真逆だった。
• ちょっと草植えときますね型言語Grass作者のid:uenoBさんとお話しできた。プログラミング言語の形式化をちゃんと考えるのは大事だねと思った。Grassはすばらしい言語だと思った。
• ET理論のalohakunさんに会った。本当にアロハシャツを着ていた。Coqを教えてくださいと言われたが、あろはさんの記事を見てCoqの勉強をしていたので、そんなのは恐れ多いです。でも、ちょっとでもCoqや論理の記事が増えるといいなと思ってる。
• Agdaの酒井さんに会った。圏論はやっぱり実際の論文とかを読んでみるのがよいと言われた。なるほど。
• INRIAに行っていたというY.Sawaさんに会った。残念ながら鶏やラクダの部署は遠かったそう。
• 懇親会ではsumiiさんとお話しできた。sumiiさんもCoqで遊びたいそうだが、忙しくてなかなか難しいそう。

ET Seminar

等価変換理論集中セミナー2008に行ってきた。
あろはさんを問い詰めるということで、朝から30人でひたすら問い詰めた。サイボウズラボの社内で行われた。
基本的にあろはさんが前でプレゼンをして、そこにリアルタイムでツッコミをいれていくという形式だった。あろはさんはいろんな人からの集中質問攻めにあって、最後の方はへとへとになってた。
おつかれさまです。個人的にはETについて少し勉強できてよかった。ETはCoqやAgdaとかよりも、自動定理証明や項書き換え系などの分野に近いのかな？と思った。
あろはさんありがとうございました。