Coq庵にいってきた

study coq

初めてのCoq(yoshihiro503)

  • 高階論理(表現力は最強)
  • 自動証明機能(tactic)を備える
  • プログラムと連携
    • 仕様が証明された状態ではなく，証明されたプログラムを書くことができる
  • tactic(小文字〜.) - Gallina式 - Vernacularコマンド(大文字〜.)
    • Vernacular と Gallina式
      • 関数の定義，問題の定式化
    • tactic
      • 証明，証明を含む式
  • Coq で書かれたプログラム
  • Coq習得の近道
    • ML や Haskell を知る
    • 書いてみる，マニュアル，Twitter，Blog
      • わからなければマニュアル
      • Twitter，Blog で困ったと言う
      • Blog で報告(解決してもしなくても)
  • さらに熟練するには
    • CPTD(Certified Program with Dependent Types)
    • Coq'Art
    • その他Curry-Howard や 型理論など

内部的には同じ意味だけど，こっちを使うとCool とか，
そういう感じなんだー．と思ったりしました．
ちょっと Coq が身近に思えました．

Coqによる暗号アルゴリズムの暗号学的安全性検証(yamakiyoさん)

  • 疑似乱数生成器 Blum Blum Shub(BBS) の実装の安全性検証
    • 実装の正しさの証明

にわとりかんさつにっき in お茶大(MoCo7さん)

一般たらいまわし関数の停止性を証明する(kikxさん)

Coqでガベージコレクションの証明(mzpさん)

  • Coq は合宿が最初
  • 中でGC が動いている
  • 気兼ねなく話せるってもんさ
  • GC 本読書会 - GC が熱い
  • ルートオブジェクト - プログラムが直接使っているオブジェクト
  • Collection モジュール
    • Ensembles
    • LisSet
    • FSets
  • 実装

ペアプルービング

- 出席できませんでした >


別件の用事があって途中退席になってしまったのが非常に残念です．
勉強の仕方がなかなかわからなかったけど，
Anarcy Proof とかで自分で考えるようになったのが
とても勉強になっている気がするので
手を動かすのはやっぱ大事だなー．
とか最近思ってることです．