[logic-ml] PPLサマースクール2017: 参加募集

[Takahito Aoto]

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%bc%e3%81%bf/
から，お申し込みください．事前登録をお願いしております．

== 問い合わせ先 ==

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

------------------------------------------------------------------------