今日、定理証明支援系の集まりproof summit 2011に行ってきました。
場所は株式会社豆蔵トレーニングルーム(新宿三井ビル34F)で、
予定通り迷いました～
でも時間までには着けた。セーフ
午前はチュートリアル
Coq,Agdaについてはほとんど初心者なのですごく勉強になりました
Coqはtacticがあって、割ととっつきやすそう。
Agdaはガリガリ書くタイプには向いてそう。
という印象でした。
でも、両方とも最後はかなり難しそうな話でした。
全国的に昼
ステーキ屋さんでみんなと一緒に食べたー
整楚帰納法について教えてもらい、やや理解が深まった感じでした。
sakaiさんありがとうございます。
午後は発表
- 自動定理証明
- Coq,Agdaを用いた応用：回路設計,ＭｓｇＰａｃｋ,正規表現
- Coq,Agdaの拡張：分離論理、代数ライブラリ、ssreflect
勉強会等の紹介
Software Foundations 日本語版
Formal Method Forum勉強会
なかなか証明の話とかで盛り上がれることも少ないのでこういうイベントは非常に貴重だと思います。
特に今回、東京だったので行きやすかったです。
こういうイベントがあるならまた行きたいです。
今後のFormal Method Forum勉強会
とかもチェックしとこう
ということでした。
終わった後
まぁ、今回が初めて参加したイベントだったので
夕飯はいつも通りぼっちかと思いきや、
同じく初参加の人と一緒に食べました。
割と突っ込んだ話とかもいろいろできて楽しかったです。
ちなみにナンでした（おかわり２回もしてしまったー）
＃＃＃ここからメモ
定理証明の使い方について考えてみた。
・関数型言語が使えるところでは使えそう
・部分部分ではきっちりと仕様が決まっていて、なおかつ巨大な構造を持つもの。
↓
・すでにあるプログラムを実装しなおすことで健全性を示す。
・回路の設計には向いてそう
・プログラムのすべてを実装しなおさなくても、モデル検査だけでも応用できそう
・他の学問の体系の実装とかできないかなー
