<div dir="ltr"># 重複して受けとられた方はご容赦ください<br><br>皆様、<br><br>筑波大の海野と申します。<br><br>日本ソフトウェア科学会第39回大会 (<a href="https://jssst2022.wordpress.com/" target="_blank">https://jssst2022.wordpress.com/</a>) 併設のイベントとして<br>8月30日（火）にオンラインで開催予定のPPLサマースクール2022「計算効果入門 ― プログラミングから理論まで ―」についてご案内いたします。<br><br>参加申し込みサイトはまだ準備中ですが、近日中に下記リンク先で公開予定です。<br><br><a href="https://jssst2022.wordpress.com/participation/" target="_blank">https://jssst2022.wordpress.com/participation/</a><br><br>一流の講師陣による講義を、参加費無料で受けられるサマースクールです。多数のご参加をお待ちしております。<br><br>---<br><br><a href="http://ppl.jssst.or.jp/index.php?ss2022" target="_blank">http://ppl.jssst.or.jp/index.php?ss2022</a><br><br>PPLサマースクール2022<br>「計算効果入門 ― プログラミングから理論まで ―」2022年8月30日(火) 10時-17時（予定）<br>オンライン開催<br><br># 概要<br>プログラムは実行中に入出力、記憶装置のアクセス、乱数のサンプル、ジャンプなど、単なる値の計算として捉えられない様々な動作をする。それらは総称して計算効果(computational effect)と呼ばれる。多様な計算効果を統一的に扱うべく、80年代後半にMoggiはモナドによるモデルを提唱した。このモデルはプログラムの挙動の理解に進歩をもたらした他、新しいプログラミング機構の導入にもつながっている。Haskellのモナド、call/ccなどの制御演算子、そして近年試験的に実装されている代数的エフェクトとエフェクトハンドラはその例である。<br><br>本サマースクールでは情報系の学部４年生・大学院生および大学・企業の研究者を主な対象とし、3名の講師が計算効果のプログラミングから理論まで、様々な話題を紹介する。受講にあたっては型付きラムダ計算、論理学、集合・関数に関する学部程度の知識を前提とする。<br><br># 講師紹介（発表順）<br>勝股 審也<br>国立情報学研究所・特任准教授およびERATO蓮尾メタ数理システムデザインプロジェクト・研究総括補佐。2005年エジンバラ大学 Ph. D。研究テーマはプログラミング言語とシステムの意味論、およびプログラム検証の数理的基盤を研究している。<br><br>叢 悠悠<br>東京工業大学情報理工学院数理・計算科学系助教。2019年お茶の水女子大学大学院博士後期課程修了。限定継続の型システムや、制御演算子・代数的効果の関係に興味を持つ。<br><br>関山 太朗<br>国立情報学研究所アーキテクチャ科学研究系・助教。2016年京都大学 Ph.D。プログラミング言語理の型システムやプログラム検証に関する研究に従事。<br><br># プログラム（予定）<br>10:00 - 10:30 計算効果の導入<br>10:30 - 12:00 限定継続を使った計算効果プログラミング<br>12:00 - 13:30 昼休み<br>13:30 - 15:00 計算効果の推論技術<br>15:00 - 15:30 休憩<br>15:30 - 17:00 計算効果の数理モデル<br><br>「計算効果の導入」（講師：勝股）<br>計算効果とはプログラムの実行時に引き起こされる多様な振る舞いの総称であり、入出力、非決定的選択、例外処理、継続の扱い、確率的選択など多岐にわたる。このセッションでは計算効果がどのように定式化され、理論的・応用的に発展してきたかを概観する。<br><br>「限定継続を使った計算効果プログラミング」（講師：叢）<br>限定継続はさまざまな計算効果の表現に有用な概念である。本講義では、限定継続の基本的な考え方を説明し、代表的な応用例を紹介する。また、限定継続を扱うことのできる言語を用いたプログラミング演習も行う予定である。<br><br>「計算効果の推論技術」（講師：関山）<br>プログラムを正しく理解・検証するためにはプログラムがどのような計算効果を引き起こすかを推論することが重要となる。本講義では(型システムを中心に)計算効果のためのプログラム推論技術について紹介する。<br><br>「計算効果の数理モデル」（講師：勝股）<br>Moggiは80年代後半に計算効果の数理的モデルとして圏論由来の構造であるモナドを使うことを提唱した。このセッションでは代数の観点からモナドを導入する。そしてモナドを用いたプログラミング言語の表示的意味論を紹介する。<br><div></div></div>