ATND アテンド β PRODUCED BY RECRUIT

ログイン or 無料登録

Coq庵

Coq Programmer's Unconference

日時 :
2010/08/29 (日) 13:10 ~ 17:30
定員 :
46人
会場 :
名古屋市青少年文化センター(ナディアパーク) [9階] 第3研修室 http://www.nadyapark.jp/traffic/(愛知県名古屋市中区栄3-18-1)
URL :
http://coq.g.hatena.ne.jp/keyword/Coq庵
主催者 :

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もよろしく


    我々ProofCafeocaml-nagoyaのメンバーを中心に名古屋で毎月第4土曜日に勉強会を行っています。Coqや検証ツールに興味のある方はこちらもどうぞご参加ください
  • このコメントは全員が閲覧、すべてのログインユーザが投稿することができます
yoshihiro503
yoshihiro503 - (2010/06/26 (土) 19:57)
短歌会館、和室(30人)、集会室(60人)は共にだめでした。2階の会議室(18人)ならokとのこと。
yoshihiro503
yoshihiro503 - (2010/06/26 (土) 20:07)
名古屋市青少年文化センター(ナディアパーク)の研修室(46人)がとれました。
mzp
mzp - (2010/08/25 (水) 21:05)
会の終了後、近場で懇親会やるかもしれまん。
時間に余裕のある人は、一緒にニワトリ(手羽先)を食べましょう!

コメントを投稿するには、ログインしてください。

掲載されるイベント情報は、利用者の皆様によりご提供いただくものであり、株式会社リクルートホールディングスは本情報の正確性や内容について、一切保証するものではございません。詳しくは利用規約をご参照ください。