osiire’s blog

ふしぎなそふとやさん

PPL2010参加

毎年恒例のPPLに参加。e-mobileがまさかの圏外で仕事的にやや不都合だったけど、今年も色々な話が聞けて面白かったです。運営してくださった皆様、ありがとうございました。とりあえず感想がかけそうなものだけ書いておきます。

  • Towards Formal Construction of Assembly Arithmetic Functions from Pseudo-code
    • 数値計算をCoqで検証するためには、32bitとかそういう制限はpseudo-codeからの変換時にやった方がいいんじゃない?というお話。フレームワークとライブラリを実際に作ってた。公開されているのかしら。
  • 極性をもたないセッション型システム
    • 自身へのチャネル渡しを含むセッション型が極性使わなくてもできるぜ!という貢献。プログラミングの世界への応用も考えると重要な成果だと思うので、個人的には一押し。別途教えてもらった所によると、この構文と型システムは推論も可能とのこと。エラーまで考えられるので、もうプロトコル記述はこの文法でよくね?
  • Self Type Constructors
    • 型パラメータの型が戻り値に含まれるようなメソッドがあるクラスについて、型パラメータに下限(や上限)を設定して継承するお話。これは知らないでやっちゃうと嵌まりそう。少なくともセンシティブな話だというのは分かったので、今後の設計では気を付けよう。Scalaとの比較もあって興味深かった。
  • オブジェクト指向言語余話
    • C++Javaの栄枯盛衰の話+ガベコレについて。Selfが一押しだったけどメインストリームにのらなくて残念とおっしゃっていた。その原因は?と質問した方がいて、「文法がC++に似てなかったから」という回答は印象に残った。
  • DrSchemeのWorldティーチパックを使ったゲームの作成
    • なんと高校生によるポスターとデモ発表。後生&お茶大おそるべし。DrSchemeのライブラリ(?)に「Teachpacks for How to Design Programs」というのがあるらしく、これでゲーム的なものを作ったよというお話。GUIを画面更新とキー入力とマウス入力で表現してて、簡素さといい教材的にもすばらしい。
  • shift/reset による Caml Light の拡張に向けて
    • shift/reset推進委員会より。Caml Lightにshift/resetを入れたぜ!というお話。まだ不具合が残るものの実装済み。すばらしい。oleg氏の方針とは異なってかなり実直(?)にやっている模様。これが出来ればOCamlへの足掛かりだし、ネイティブコンパイルも夢じゃないので期待大だと思った。
  • 汎用的に証明木のGUIを作成する『Mikiβ』の開発
    • 証明木をGUIで作成するお話。もちろんOCaml+lablgtk。推論規則などを記述すれば単純型付きラムダ計算以外も任意にサポートできるので「汎用」。論理学の勉強にすごく使えそうなので、使ってみたい。(公開されてるのかなー?)
  • Small-step and Big-step Semantics for Call-by-need
    • small-stepとbig-stepの同値性は当然だよね?と思われていたけど、全然自明じゃなかったよ、でも証明できたよ、というお話。こういうツッコミはとても重要だとおもた。

私はソフトウェア科学会の回し者じゃないけど、PPLとかいわゆる学会って敷居が高い気がするものの、意外と得るものが多いので企業のみんなも参加するといいヨ!(予算的にはやや敷居が高いのは否めないけど)