ProofSummit2014とJSSST2014に参加

event Coq

遅めの夏休みを使ってProofSummit2014とJSSST2014に行ってきました。

Coqチュートリアルとサマースクール(スパコンの話)に参加し、火曜日のPPLとその他セッションをふらふらしてた感じ。


Coqチュートリアルが主目的で参加したハズなんですが、謎の強烈な眠気であんまり覚えてません…。ひどい。
ssreflectのタクティックはかなりゴルフ的な方針で証明を短くしている感じを受けた気がします。
あとはかなり所謂工数を気にかけてCoq採用事例が解説されていたのが印象的でした。まだ開発で採用されるには時間がかかると思っているのですが、気づいたら証明も出来ない奴は人権が無い世界になるかも知れません。コワイ。


スパコンのサマースクールでは学部の授業を大急ぎでなぞった感じであまりテクニカル(に最新)な話は出ませんでした。
20年後でも使える言語じゃ無いとダメだそうですが、20年前に出来たソフトを使い続けてるんでしょうか。


他で印象に残ってるのは筑波の方のrefinement typeの拡張(?)とガリグ先生の型エイリアスでしょうか。PPL4
前者は自分で質問したのでやはり覚えてますね。
提案手法(述語を何回か展開して近似)では SMTソルバのfixpoint operatorより一般的なケースを扱えるようです。オフラインで教えて頂いたのですが、使ってるのはまさに質問で持ち出したZ3だったようで発表者の方にはその場で答えて欲しかった内容ですね(笑
それはともかくSMTソルバ流行ってますねぇ。


後者はOCamlモジュールの代入は通常定義をコピーするのに対して、名前を追跡するようになるものと理解しました。
アプリカティブファンクタに有用とのことですが、SMLにあっても嬉しいような気がします。どうなんでしょう？
あとNJ(というかCM)がさりげなく槍玉に上げられていたのでOCamlにだって仕様は無いじゃないか ( ｰ`дｰ´)と言っておきます(笑


FTDが初日のチュートリアルと被ってたので今回は会場で観られませんでした。
ちょっと残念でしたね。youtubeで公開してるので一応リンク貼っておきます。