ProofSummit2011

Formal Methods

告知

http://partake.in/events/ac41261d-6026-4d09-8814-5ad3e58446e8

Ustream

http://www.ustream.tv/channel/proofsummit1#utm_campaign=t.co&utm_source=9389178&utm_medium=social

togetter

http://togetter.com/li/192747

出席者(自主的に記入してくだされ)

https://docs.google.com/spreadsheet/ccc?key=0Akg8l0azZuMsdG9QTVcydHRiMVZtSXlkbkxDNFJzWGc&hl=ja#gid=0

InfoQ記事

http://www.infoq.com/jp/articles/ProofSummit2011

Coq入門質疑応答メモ

Agda入門質疑応答メモ

  • スライド
  • 空白に厳しい言語です。
  • アンダースコアは予約語です。
  • if_then_elseのアンダースコアとキーワードの間の空白はなしですか。
    • なし。全部つなげて書きます。
  • アンダースコアは連続してはおけないんですか?
    • そうです。
  • Lazyな言語なんですか?
    • Backendが何かによって変わります。
  • 変数束縛はありますか?
    • syntaxで作ります。mixfixではない。
  • do式はできる?
    • bindがあればできるはず。
  • 型パラメータのお話:省略可能引数を省略しないで書くときは?
    • 中かっこで明示します。
  • 「かつ」はシンメトリックになってるはずだが、そう読めないんだけど。
    • 証明しましょう。
  • 証明できないこと。でaxiomを入れることはできるんですよね。
    • できます。
  • unitはないんですか?ocamlではunitは()なんですが。
    • Agdaでは()はパターンの書き方です。特別な意味を持っています。
    • AgdaのunitはT(bottomをひっくり返した形)です。
  • withパターン。インデントをずらしたらどうなっちゃうの?
    • インデントをずらしたことがないのでわからないです。
    • Haskellだと意味が変わってしまう。
  • withが2つつくような場合は?
    • withの後ろにどんどん宣言していけばよい。
  • Agdaはcase文がないです。Agda1にはcase文あるのに。
    • caseで書いた関数を証明するときにうまくいかなかったことがあったのでなくなったとか。
  • dotパターンは何個でも書ける?
    • はい書けます。
  • dotがつかない、かつなんかのコンストラクタになる(パターンマッチになってる)ものは?
    • 書けます。
  • 次のバージョンからAgdaはデフォルトでmutualになるの?
    • そうです。
  • Agdaは読み込み時に、コンパイルが行われます。
  • Javaのクラス名、ファイル名と同様、Agdaでも大文字小文字を識別しますか?
    • たぶん識別してるはずです。
  • Agdaではデータ型として等号が定義されています。
  • SizedType。divならば楽だが、もっと難しいもので、対話的に停止性を与えたいときはどうしますか。
    • 記述は可能だがあまり役に立たないかも。
  • Epicって関数型言語ですか?
    • ちょっとわからない。->要調査(Epic:equational programming languageかな)
  • Coqでも関数記述できます。が、関数定義は何の支援もないです。Agdaでは関数定義時にツールの支援があります。
  • agda_in_browser
  • Agdaで時計の何が証明されてるんでしょうね。
    • 要調査?

CoqによるMsgPackシリアライザの証明と実装

  • Coqのコードも公式リポジトリに入ってますよね
    • 入ってます。
  • あなぷるに出題した問題ってどれですか?
    • 変換関数の性質の証明です。
  • オーバーフローの回避するとき、Zを使うという手はなかったのか。
    • 便利なライブラリを使いたかったのです。OCamlのコード変換時のライブラリ。
  • natとintのextractionはunsafeです。

START SEPLOG + COQ2

  • スライド
  • Sepalation Logicでは状態も与えないと真偽が決まらない。
  • Coq上で、C言語のインタプリタを作っていく。
  • stateがオプションなのはなぜですか?
    • 終状態と始状態の型があっているほうが証明しやすいからだと思われます。
  • 三項関係にしたのは停止しないプログラムを書けないからだ、というが・・・
    • 停止問題自体は解かなければいけない。
    • 三項関係を定義することと、特定の三項関係の停止性を証明することは別問題。
  • Caracteristic Formulae
  • Local variable
    • Local variableはストア
    • アドレスがheapになる
    • swapするときの動作は?
  • ホーア論理
    • 止まるなら成り立つ、必ずとまる、の２種類の３項関係がある。
  • 非決定的なもの、並行処理は記述できるのか?
    • Concurrent Separation Logicというのがあります。
  • CにExtractできるの?
    • むしろCのコードからCoqに変換して証明するながれ。
  • 実行コンテキスト（スレッドが違う）とかは考慮されてないですよね。
    • そうです。

ssrefrect

  • by do 2 case.のときにreflexivityはかかなくてもいい?
    • byは簡単な証明はやってくれるので、書かなくて良い。
  • move: x y z => a b.のとき、x y zは仮定になくてはいけない?
    • そうです。
  • byとtry doneの違いは?
    • byは失敗を知らせてくれる。
    • doneでだめだったときは、by autoを試す。
  • unfoldもrewriteで表現するんですか?
    • そうです。
  • Coqのソースがどの程度へりますか?
    • ほとんど減りません。rewriteの文字は圧倒的に減ります。
  • あなぷるでssreflect対応が入るのはいつですか?
    • そろそろ対応?
  • ssreflectでは、証明できることは同じ?
    • 同じです。
  • Coq8.3対応もしてますが、trunkを使わないといけない。
  • ssreflectのWindows版を見つけたんですが、linux版はないんですか?
    • ありますよ。
  • なんでMicrosoft Researchの人がやってるの?
    • 四色問題やってるのもMSでしたが、理由はわかりません。
  • 証明スクリプトの停止性は別の話。

LT