PPLサマースクール2017 「Isabelle/HOL による証明とプログラミング」 http://ppl.jssst.or.jp/index.php?ss2017
----
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 をストレスなく利用するために，ある程度高性能なノートパソコンを推奨します．
受講にあたっては，簡単な証明を書ける程度の基本的な論理学の知識を習得していること，また関数型言語の利用経験があることが推奨されます．
#ns