Coqプログラマーの集会を名古屋で行います

証明支援器Coqは形式手法の一つである定理証明のためのツールですが、Coqのプログラミング言語としての側面や、Coqでソフトウェアを開発できることは産業界においてあまり知られていません。
Coq庵は、Coqを用いたプログラミングや、Coqを用いたソフトウェア設計と安全性の検証にフォーカスし、自由な情報交換を目的としたアンカンファレンスです。

バグのないプログラムの開発、関数型言語や形式手法に興味のある方など ぜひともご参加ください。

• 参加費: 200[円]


• 時間: 13:15 – 17:30


• twitterハッシュタグ: #CoqUn

話者募集

• Coqについて話をしたいという方を募集します。
  ここのコメントか、下記のメールアドレスにご一報ください。 *)
  締め切りました。
  

  
  
  Require Import String.
  
  Eval compute in (“y.imai” + “@” + “ocaml.jp”)%string.
  
  

  
  

  プログラム

  
  
  
  
  • 13:15 受付、はじめのことば
  
  
  • 13:30 初めてのCoq(yoshihiro503)
  
  
  • 14:00 Coqによる暗号アルゴリズムの暗号学的安全性検証(yamakiyoさん)
  
  
  • 10分休憩
  
  
  • 14:40 (MoCo7さん)
  
  
  • 15:10 一般たらいまわし関数の停止性を証明する(kikxさん)
  
  
  • 15:40 Coqでガベージコレクションの証明(mzpさん)
  
  
  • 10分休憩
  
  
  • 16:20 ペアプルービング
  
  
  • 17:20 おわりのことば
  
  
  
  

  ペアプルービング お題

  
  ペアプルではkikxさんが作成したanarchy proofのお題に挑戦しましょう。自分なりに作った証明を投稿して通れば正解です。kikxさんには大感謝です。
  

  前日はOCamlMeeting

  
  前日には名古屋大学でOCaml Meeting 2010が行われます。Coqユーザーなら参加しておきたいですね。
  

  ProofCafeもよろしく

  
  我々ProofCafeはocaml-nagoyaのメンバーを中心に名古屋で毎月第4土曜日に勉強会を行っています。Coqや検証ツールに興味のある方はこちらもどうぞご参加ください