アフェルト レナルド博士
概要
- 日時
- 2014年9月7日(日) 14:00-18:00
- 講師
- アフェルト レナルド
- 産業技術総合研究所主任研究員
- 会場
- 名古屋大学東山キャンパス IB電子情報館１階 IB015
内容
数学とソフトウェア科学の両方の分野において，定理証明支援系への関心が高まっています．なかでも，フランス国立情報学自動制御研究所（INRIA）で開発が進められている定理証明支援系Coqは，ACM SIGPLAN Programming Languages Software 2013 AwardとACM Software System 2013 Awardの受賞を契機に，より多くの研究者や技術者の注目を集めています．Coqは，四色定理の証明に代表される数学分野での貢献だけでなく，ソフトウェア開発への応用においても大きな役割を果たしてきました．
本チュートリアルでは，産業技術総合研究所のアフェルト レナルド氏をお招きし，モダンなCoq入門の観点から，Coqの拡張であるSSReflectを使った証明の初歩を紹介していただきます．SSReflectはタクティクスの表現力が向上し，数学の膨大な証明が可能になっただけでなく，プログラムの検証でも伝統的なCoqに代わって使われるようになっています．定理証明支援系を使った証明に関心を持つ研究者や学生の方，ソフトウェアの形式検証に関心を持つ研究者や技術者の方など，多くの方々の参加をお待ちしております．
（本チュートリアルは日本語で行います）
チュートリアル資料
チュートリアルのスライド，Coqファイル，Coq/SSReflectの設定情報，Coqのcheat sheetは，アフェルトさんのサイトから提供されます．現時点ではアフェルトさんが鋭意執筆中ですが，最終版は9月6日（金）の晩には公開されます．資料は事前にダウンロードしてお持ち下さい．このサイトでも一時、zipを配布していましたが、さらに最新の物がアフェルトさんのサイトで公開されています。
アフェルトさんからのメッセージ
Coq/SSReflectを動かさなくても聞ける発表にするつもりですが、参考としていくつかのCoqファイルを用意します。また，Coqファイルの理解のため、 追加資料として、cheat sheetを作ってみました．
参加要領
参加費
| 区分 | 一般 | 学生 |
|---|---|---|
| 会員 | 3,000 円 | 1,000 円 |
| 非会員 | 5,000 円 | 2,000 円 |
- 募集定員
- 60名
- お申し込み方法
- 大会参加申し込みページからお申し込みください．
- 本チュートリアルはPPLサマースクールと連携しており，サマースクールに引き続いて行われますが，サマースクール参加者の方が本チュートリアルに参加される場合にも，上記からのお申し込みが必要です．
プログラム
- 14:00-15:00:
Part 1: 定理証明支援系とは- 定理証明支援系の概要
-
定理証明支援形の歴史
-
定理証明支援系の応用例
- ソフトウェアの形式検証
-
数学の証明の形式化
-
15:00 – 15:15 休憩
-
15:15 – 16:15
Part 2: 定理証明支援系Coq/SSReflectの入門- Coqによる形式証明の原理
-
CoqとSSReflectの違い
-
形式モデルと仕様の作成
-
形式証明の基本
-
16:15 – 16:30: 休憩
-
16:30 – 17:30
Part 3: SSReflectライブラリの紹介- SSReflectライブラリの概要
-
基礎ライブラリ
-
総和と総乗
-
群と代数
-
17:30 – 18:00
Part 4: 関連するトピックス- 命令型プログラミング言語の検証
- アセンブリ言語への応用
-
C言語への応用
-
数学の証明の形式化
- 情報理論の形式化
-
符号理論の形式化
- 命令型プログラミング言語の検証
（プログラムは変更される場合があります）
日本ソフトウェア科学会 第31回大会 