#ProofSummit 2014 ## 概要 定理証明支援系(Coq,Agda,Isabelle/HOL,ACL2などなど)や自動証明器などを中心に集まるお祭りです。 - 日時: 2014年09月06日(土) - 場所: 名古屋大学 多元数理科学棟 109? - 参加費: 無料 - 参加登録: [ProofSummit 2014 - Partake](http://partake.in/events/b01d8f2b-d0e9-4b48-96ac-ed633dce83d4) - 持ち物: おやつ、(電源タップ)、(PC) ## プログラム |時刻 |発表者(敬称略) |所属 |内容 | |------------|------------------------------------------------|----------------|--------------------------------------------| |10:00~ |[今井宜洋](http://proofcafe.org/~yoshihiro503/) |[ITプランニング](http://www.itpl.co.jp/)|オープニング | |10:10~10:40 |[今井宜洋](http://proofcafe.org/~yoshihiro503/) |[ITプランニング](http://www.itpl.co.jp/)|放送事業におけるCoqの使用| |10:40~11:20 |chiguri | |VSTでCの検証 | |11:20~12:00 |[@dico_leque](https://twitter.com/dico_leque) |[ITプランニング](http://www.itpl.co.jp/)|Proof and Emacs(仮) | |12:00~13:30 | | | 昼休憩 | |13:30~14:20 | [@kikx](http://twitter.com/kikx) | |(* CoqでOpenSSLのバグを見つけた話 *) | |14:20~15:00 |才川隆文 |名古屋大学 | HoTT関連(TBA) | |15:00~15:30 | | | おやつタイム | |15:30~16:10 |木下修司([@kiiiino3](https://twitter.com/kiiiino3))| | Agdaを使った形式化の実例紹介 | |16:10~16:50 |notogawa | | Real World Agda (仮) | |16:50~17:30 |@Alcor80UMa (岡崎裕之) |Stowarzyszenie Uzytkownikow Mizara (信州大学) |Mizarによる形式証明の簡単な実例| ## 主催・協力 - [有限会社 ITプランニング](http://www.itpl.co.jp/) - [ProofCafe](http://proofcafe.org/wiki/) - [Formal methods forum](https://groups.google.com/forum/#!forum/fm-forum) ## 連絡・お問い合わせ先 - twitter: [@yoshihiro503](http://twitter.com/yoshihiro503) - mail: yoshihiro503 at proofcafe.org