SML/NJまわり
id:sumii先生からは大堀先生のSML#についてお勧めいただいた．しかしSML#は色々新しい着想に基づいてるようで，MinCamlを追うのもいっぱいいっぱいな私にはそれすらまだ早いかな．
ただまぁ一応SML/NJについてのメモ．SML/NJが「すさまじい」というのは google:"sml/nj proof soundness" から辿った以下のスライドで知った．
- http://www.eecs.umich.edu/acal/swerve/docs/123-2.ppt Automatically Generating Foundational Proofs for Program safety
↑のスライドは解説抜きでは具体的な内容がさっぱり分からん．同じテーマについて少し詳しい文書はこちら：
- http://www.cs.princeton.edu/~dinghao/papers/checker.pdf Foundational Proof Checkers with Small Witnesses
要するにSML/NJの後ろに型付きアセンブラと，そのレベルで健全性を証明するシステムをくっつけたらしい．WuさんはAppelの（元）学生で，この話をD論にまとめた*1ようだ．それがこちら↓
- http://www.cs.princeton.edu/~dinghao/papers/wu_thesis.pdf Interfacing Compilers, Proof Checkers, and Proofs for Foundational Proof-Carrying Code
全く読んでないのでアレだが「Givenなものとして与えた定理たちをうまく選んだから全体的にすっきりしたよ」と言っているが，定理証明系の入力に165k行とか言われると... それともこれは自動生成されたということ？
Shao先生というのはYaleの教授ですか．彼の中間言語プロジェクトFLINTが合流したせいでSML/NJのコードがすさまじくなったということですかね．
本題からずれるが... うーん，ACM/ICPCでは私の数十倍から百倍の実装力を持つ日本のトップ勢ですら残念なことに中国勢に及ばない現状があるけど，そういう中国人が Princeton → MS研 と動くのが今の流れなのか．
