PPLサマースクール2017
Isabelle/HOL による証明とプログラミング
 
日本ソフトウェア科学会 (JSSST) プログラミング論研究会 (PPL) 主催
日本ソフトウェア科学会第34回大会 併設企画
Webページ: http://ppl.jssst.or.jp/?ss2017
 
講師：山田 晃久(インスブルック大学)
 
2017年 9月 18日 (月) 10:00 - 17:00
慶應義塾大学 日吉キャンパス
 

概要 †

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回大会共通の 参加登録ページ からお申し込みください． 事前登録をお願いしております．

↑

問い合わせ先 †

PPLサマースクール2017 幹事
青戸等人 (新潟大学)
E-mail: aoto [at] ie [dot] niigata-u.ac.jp

↑

過去のサマースクール †