文書の過去の版を表示しています。
PPLサマースクール2017
Isabelle/HOL による証明とプログラミング
日本ソフトウェア科学会 (JSSST) プログラミング論研究会 (PPL) 主催
日本ソフトウェア科学会第34回大会 併設企画
Webページ: http://ppl.jssst.or.jp/?ss2017
講師：山田 晃久(インスブルック大学)
2017年 9月 18日 (月) 10:00 - 17:00
慶應義塾大学 日吉キャンパス来往舎 1F シンポジウムスペース
(〒223-8521 神奈川県横浜市港北区日吉4-1-1)
ニュース
- 会場詳細を追加しました．受付は会場前にございます(9/13)．
- 受講者へのご連絡を追加しました(8/30)．
概要
Isabelle/HOL は，1986年に Lawrence Paulson によって創始され，現在はミュンヘン工科大学 Tobias Nipkow のチームを中心にメンテナンスされている証明支援ツールです．
Isabelle/HOL の特徴は，スマートな証明環境 (jEdit)，強力な自動証明のサポート (Sledgehammer)，Haskell 等への自然なコード輸出 (code export)，多彩でオープンなライブラリ (Archive of Formal Proofs; AFP) などが挙げられます．
本セミナーでは，Isabelle/HOL を用いた定理証明と，正しさの保証されたプログラム開発方法を，実践を通して紹介します．また AFP より，代数的数計算ライブラリなど，そのごく一部を紹介します．
Isabelle には歴史的経緯からさまざまなクセがあり，学習を困難にしている要因となっていると考えられますが，本セミナーでは証明言語 Isar による，クセを排した“行儀のよい”証明の書き方に徹します．
実習形式で行いますので，受講に際してはノートパソコンをご持参ください．なお，Isabelle/HOL をストレスなく利用するために，ある程度高性能なノートパソコンを推奨します．
受講にあたっては，簡単な証明を書ける程度の基本的な論理学の知識を習得していること，また関数型言語の利用経験があることが推奨されます．
講師紹介
インスブルック大学ポスドク．項書き換え系の停止性証明法に関する研究で，2014年名古屋大学情報科学研究科博士課程を修了．同年，産業技術総合研究所にて組み合わせテストツール Calot の開発に従事．2015年より，インスブルック大学にて項書換え系，プログラム解析技法などの形式証明ライブラリIsaFoR の開発プロジェクトに参加．情報処理学会正会員．
プログラム
| 9:30 - 10:00 | 受付 |
|---|---|
| 10:00 - 12:00 | 第1部 |
| 12:00 - 13:30 | 昼休み |
| 13:30 - 15:00 | 第2部 |
| 15:00 - 15:30 | 休憩 |
| 15:30 - 17:00 | 第3部 |
参加費・参加申し込み
PPLサマースクールの参加費は以下の通りです．
学生会員1000円, 学生非会員2000円, 一般会員2000円, 一般非会員3000円
参加ご希望の方は 日本ソフトウェア科学会第34回大会共通の 参加登録ページ からお申し込みください． 事前登録をお願いしております．
受講者へのご連絡
- 受講に際してはノートパソコンをご持参ください．
- 快適な証明環境のためには，ある程度高性能なマシンが必要です．HDD/SSDの空き容量が10GB，メモリが1GB以上の(相応なCPUを積んでいるような)マシンならば大丈夫と思われます．
- 事前に， https
に従って Isabelle をインストールし，一度起動しておいてください．
- 初回の立ち上げにはしばらく時間がかかりますが，二度目以降は高速になります．
- チュートリアルは Isabelle2016-1 を対象に行う予定です．他のバージョンでは操作が異なることがありますが，Isabelle2015以降であれば対応可能です．
- 上記のウェブページにあるように，オフィシャルな対応OSは，Linux, Windows 7以降，Mac OS 10.8以降です．Linux については，比較的最近のものであれば大丈夫と思われますが，必要な requirements については，上記ウェブページに記載があります．
問い合わせ先
PPLサマースクール2017 幹事
青戸等人 (新潟大学)
E-mail: aoto [at] ie [dot] niigata-u.ac.jp
過去のサマースクール
- 第6回 PPLサマースクール (PPL Summer School 2008)
今日から使える! みんなの静的解析・バグ検出ツール - 第8回 PPLサマースクール (PPL Summer School 2010)
マルチコア時代の新言語 - 第9回 PPLサマースクール (PPL Summer School 2011)
クラウドのプログラミング - 第10回 PPLサマースクール (PPL Summer School 2012)
関数型言語ベースの先進的Webフレームワーク - 第11回 PPLサマースクール (PPL Summer School 2013)
高階モデル検査とその応用 - 第12回 PPLサマースクール (PPL Summer School 2014)
高性能計算のプログラミングの最前線 - 第13回 PPLサマースクール (PPL Summer School 2015)
プログラミング言語のゲーム意味論 - 第14回 PPLサマースクール (PPL Summer School 2016)
商用Java処理系の研究開発