ICFP 2010 実況など
-
- いいね！0
kinaba
@kinaba
#WMM Appelの招待講演：静的解析器で不変条件を挿入→（以下Coqで）検証→公理的意味論から操作的意味論から双模倣で証明しやすい操作的意味論からLeroyのCompCertで抽象マシン語にコンパイルしてからPPCへ、という、並列性を扱えるCコンパイラツールチェインについて。
2010-09-25 23:39:52
kinaba
@kinaba
#WMM システムコールやpthreadはオラクルとして抽象化してやる。"この量の証明は機械化証明なしでは無理"、"証明のモジュール化(module,依存型,型クラス)重要"/(感想)それでもまだモジュール化機構が"足りてない"感を感じるけど証明言語は将来どうなるかなー
2010-09-25 23:50:59
kinaba
@kinaba
#WMM Nominal Isabelleの招待講演：「α変換を上手く仮定して変数名は変にぶつからないとする」という規約はプログラミング言語に関する証明には無いと全てが異様に複雑化して死ねるのですが、機械化するとこの複雑化がもろに降りかかって全員死ぬ、というのがこの分野最大の問題
2010-09-26 04:22:43
kinaba
@kinaba
#WMM （…と先程@chunjp に説明したら"なんで？"と一蹴されたけどえーと、やればわかる！）のを何とかする試みの一つ。データ型宣言時に"名前だ"（束縛順/未使用変数が影響する/しない等のモード付）と指定すると、それ関係の帰納述語に対し自動で名前考慮済帰納法を示してくれる等
2010-09-26 04:22:48
kinaba
@kinaba
#WMM Olegさんらのマルチステージ+shift/resetの型システムの初の機械証明の話： twelfで。現在はscope侵犯が起きないように防衛的に暗黙にreset入れる場合限定(？)。"progress"の証明とevalの定義が一体化したような記述になってて面白かった
2010-09-26 04:29:16
kinaba
@kinaba
#WMM Cheneyの「"既にある物を検証する"だけじゃなくて、定理証明系の存在を前提にして言語をデザインするとかそういう方向がそろそろあっていいんじゃないの？」という提案： 面白かった。W3C標準として定期的にDSLが作られているわけだけど、そこを乗っ取るのだ！(意訳)など等
2010-09-26 04:37:11
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
自分の発表はないのですが委員などの関係でICFP 2010に来ています。併設ワークショップを含め、内容がありすぎて実況できません…
2010-09-26 05:46:23
kinaba
@kinaba
#WMM Montagu&Remyの、最近のPOPLで提案されてた何か綺麗な存在型のシステムF^zipを定理証明系でやったよという話：Coq(+UPenn Lib.)+Ott+LNgenを使用、と。LNgen http://bit.ly/at8RNT って知らなかった便利そう
2010-09-26 06:04:46
kinaba
@kinaba
そして Nominal Isabelle の話を聴いたら午後のHOASとLocally namelessの招待講演も聴いて比較理解すべきだった気がしたけど、MSFP の方が面白そうだったのでフラフラと惹かれてそっちに来ている
2010-09-26 06:08:18
kinaba
@kinaba
#MSFP 「○×ゲームとチコノフの定理と二重否定移動の共通点は何か？」：大変おもしろかった。後で長くまとめるかも。："Quantifier"は"Selection Function"で特徴づけられる。Drinker Paradox、最大値の定理、中間値の定理…は全て共通の構造
2010-09-26 06:22:58
kinaba
@kinaba
#MSFP これらselectionには「チコノフの定理=コンパクト空間の積空間はコンパクト」に依って積や無限積を定義することができて、複雑なquantifierが作れ、例えば∃∀∃∀...（やsup inf...）という積は二人ゲームの必勝戦略を表す、とHaskell実装でデモ
2010-09-26 06:27:04
kinaba
@kinaba
#MSFP 浅田さん： Haskell等のArrowに関する圏論的な話。詳細は僕はまったく理解できてないけど要するに 「function：relation = functor：profunctor = Strong-Monad：Arrow」 だそうだ。
2010-09-26 06:29:26
kinaba
@kinaba
#MSFP Hindly-Milnerの型推論の綺麗な再定式化の話： これも楽しかった。あとで実装しよう。しかしどっかでこのやり方見た記憶があるんだけど気のせいかな…。要は、型コンテキストを、「set of 変数の型情報」でなく、「list of 変数の型 or 型変数導入」…
2010-09-26 06:35:33
kinaba
@kinaba
#MSFP …と型変数の導入をexplicitにして、unificationが必要になると「変数のスコープがおかしくならない最初の位置に変数導入を動かす」とする。と、letの型推論が始まるときにマーカーを入れてマーカー超えなかった分を汎化、とlet多相がなる、などなど
2010-09-26 06:37:18
kinaba
@kinaba
#MSFP "Epigram prime"：Epigram http://www.e-pig.org/ のデモ。拡張子がpigでEpigramマニュアルにはEmanuelとか名前がついておる…。デモ自体は初歩的すぎて結局最後までCoqやIsabelleとの差が一つも見えなかった…
2010-09-26 06:55:22
kinaba
@kinaba
#WGP C. McBride の招待講演：Typed Term（≒静的型付きDSL）を綺麗に書くには…単にtermと型チェッカを書くのではなく、termの文法定義自体に型整合性がマジカルに埋め込まれているような素敵な書き方で書くには、という楽しい問題があります(続)
2010-09-27 00:07:38
kinaba
@kinaba
#WGP 続)スコープの面倒をマジカルに見るにはNested Type。単純型ならGADTで行ける。では依存型のある埋込DSLを作るには？依存型があればＯＫ！と、まあ実際は事はそう簡単でないのですが、ホスト言語の依存型を上手く掠ってきてそれを綺麗に実現するテクニックの話。面白かた
2010-09-27 00:16:20