PPLサマースクール2017のご案内です． (重複して受信された場合はご容赦願います．)
PPLサマースクールは，日本ソフトウェア科学会・プログラミング論 研究会主催のイベントです．今回も，例年と同様に日本ソフトウェア 科学会大会の併設企画として開催いたします．
今回のテーマは「Isabelle/HOL による証明とプログラミング」で， 講師はインスブルック大学の山田晃久様にお願いしております．
参加申し込み方法などを含む詳細につきましては， http://ppl.jssst.or.jp/?ss2017 をご覧ください．是非ご参加をご検討いただければ幸いです．
--- 青戸等人(新潟大学)
------------------------------------------------------------------------
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 をストレスなく利用するために，ある程度高性能なノー トパソコンを推奨します．
受講にあたっては，簡単な証明を書ける程度の基本的な論理学の知識を習得し ていること，また関数型言語の利用経験があることが推奨されます．
== 講師紹介 ==
山田 晃久 (やまだ あきひさ) http://cl-informatik.uibk.ac.at/users/ayamada/
インスブルック大学ポスドク．項書き換え系の停止性証明法に関する研究で， 2014年名古屋大学情報科学研究科博士課程を修了．同年，産業技術総合研究所 にて組み合わせテストツール Calot の開発に従事．2015年より，インスブル ック大学にて項書換え系，プログラム解析技法などの形式証明ライブラリ IsaFoR の開発プロジェクトに参加．情報処理学会正会員．
== 参加費・参加申し込み ==
PPLサマースクールの参加費は以下の通りです．
学生会員1000円, 学生非会員2000円, 一般会員2000円, 一般非会員3000円
参加ご希望の方は，日本ソフトウェア科学会第34回大会共通の参加登録ページ https://jssst2017.wordpress.com/%e5%8f%82%e5%8a%a0%e7%94%b3%e3%81%97%e8%be%b... から，お申し込みください．事前登録をお願いしております．
== 問い合わせ先 ==
PPLサマースクール2017 幹事 青戸等人 (新潟大学) E-mail: aoto@ie.niigata-u.ac.jp
------------------------------------------------------------------------