第５回プログラミングおよびプログラミング言語サマースクール

(PPL Summer School 2007)

URL: http://www.jaist.ac.jp/~mizuhito/ppl_ss07/

開催日時: 2007年9月11日（火）＊終了しました。多数のご参加ありがとうございました＊

会場：奈良先端科学技術大学院大学情報科学研究科大講義室 (L1) ( 交通アクセス，キャンパスマップ)

主催：日本ソフトウエア科学会・プログラミング論研究会 ( 日本ソフトウエア科学会第24回大会併設企画)

PPLサマースクールは、プログラミングの理論と実践に関する基礎知識やホット・トピックに関して、分かりやすく解説していただくことを目的とした、日本ソフトウエア科学会・プログラミング論研究会主催のイベントです。第５回目となる今回も、前回までと同様、日本ソフトウエア科学会大会併設企画として開催されます。プログラミングの理論と実践に関して興味のある学生、企業・大学の技術者および研究者、また自分の専門外の分野についての知見を深めたい研究者などが対象です。

今回のサマースクールでは、厳選された３つのテーマに関して、それぞれ第一線の研究者を講師としてお招きし、わかりやすく解説していただきます。もっとじっくり話を聞きたいという過去のサマースクール参加者の皆さんの声を反映して、各講師の先生にはたっぷり２時間かけてお話ししていただく予定です。また従来同様、参加費も非常に低く設定しています。多数の皆様のご参加をお待ちいたしております。

幹事より一言

落語の三題噺のようですが、今回の３つのテーマは個人的な問題意識に発しています。現在、組込みシステムなどリアルタイム性の高いソフトウェアが注目されています。ともするとハードリアルタイムシステムなどを想定した定量的なモデル化が前提となりがちですが、その前に非同期処理やマルチコアを念頭においた定性的なモデル化ならびに定性的モデルに基づく形式検証手法が研究のターゲットになるのでは、と感じています。
小野諭先生（工学院大学）には、その豊富なリアルタイムシステムの開発経験をもとにした記述モデルやデザインパターンをお話していただきます。それに続き、これはぐっと理論的になりますが、リソースの性質記述を考慮に入れた一群の論理体系として部分構造論理に着目し、小野寛晰先生（北陸先端大）に部分構造論理の証明論的側面のお話をお願いいたしました。最後は、近年、その高速性と使い易さゆえ注目を集めている命題論理のSAT solver の使い方を広川直先生（北陸先端大）に停止性自動証明ツールへの応用を例に紹介していただきます。
この３つの講演は (1) リアルタイムソフトウェアの定性的モデル化、 (2) リソースを考慮にいれた性質記述、(3) 健全な近似の後に充足検査器による自動検査、という将来の研究の流れに対応するもの、と夢想していますが、はたしていかがなるものか、それは将来のお楽しみです。
なお今回は、講師の先生方と歓談する機会としてレセプション（無料）を終了後行います。ワイン・ソフトドリンクとチーズのみをお出しする程度ですが、それも併せてふるってご参加ください。お待ちしております。

プログラム

9月11日(火）

10:00-10:30 受付

10:30-12:30
非同期リアルタイム処理（デヴィットカトラーの見果てぬ夢）

講師：小野諭（工学院大学） OHP photo1 photo2

概要：本講演では、並行性（Concurrency) をもつリアルタイム処理について、開発経験談を交えながら、記述モデル、デザインパターンなどをサーベイする。
近年、シングルCPUのクロック上昇が行き詰まり、マルチコア化が進展している。また、Linux, Windows などの商用汎用（非実時間）OSは、こうしたハードウェアの特徴を生かすため、SMP（対称マルチプロセッサ）対応と、カーネルマルチスレッド化が積極的に行われている。
本講演では、このような汎用OSに、SMP対応のリアルタイム機能拡張を行う手法について、機能要件、統一した記述モデル、典型的なデザインパターン、開発事例にもとづく留意事項などを説明する。記述モデルとしては、多重コンテキスト、非同期、非逐次化の３つを特徴とするオブジェクトモデルを用いる。このモデルは、SMPできわめて効率よく実装でき、また、高いスケーラビリティにより高多重度・高速ネットワーク処理が容易、さらに計算のキャンセルや電源障害などの非同期イベントの正確な制御が可能など、高性能・高信頼な実時間処理記述において、大きな利点を持っている。
この記述モデルは、古く１９７０年代に開発された DEC社RSX-11, VAX/VMS などの実時間OS, 汎用OSにおいて、カーネル実装や実時間組み込みソフト記述に採用されたモデルである。その起源は、DECからMicrosoft に移り、WindowsNT の開発を指揮した David Cutler の発案に基づくものと考えられている。本講演では、こうした歴史的背景にさかのぼりながら、通常の Unix, POSIX API とは異なる本記述モデルの発展・受難と復活の流れについて、個人的見解を語る。

12:30-13:45 昼食・休憩（受付は 13:00-13:45開設、それ以降は会場の幹事・小川までお願いします）

13:45-15:45
Substructural Logics ---- 証明論的視点から

講師：小野寛晰 (北陸先端科学技術大学院大学) OHP Related photo1 photo2

概要： Substructural logics (部分構造論理）の研究はこの２０年間ほどの間に大きな発展を遂げてきた。Substructural logics は Lambek 計算、relevant logics、linear logic、多値論理などの多くの代表的な非古典論理を含んでいるが、その基本的な体系の形式化にはシーケント計算が用いられている。それでは、シーケント計算を用いることがこれらの非古典論理の理解のためになにか本質的な意味を持つのだろうか？
この講演では最近の substructural logics の研究成果をふまえ、この問いに対する一つの解答をあたえるとともに、シーケント計算による形式化の特質を改めて検討してみたい。
（補足）講演では、技術的な内容よりも概念的な解説に重点を置くので、論理についての基本的な知識のみを仮定する。

16:00-18:00
停止性自動検証ツールにおける SAT Solver の使い方

講師：広川直 (北陸先端科学技術大学院大学) OHP photo1 photo2

概要：項書換えや関数型言語のプログラムの停止性を自動証明するツールは、この5年間で証明能力・実行速度ともに飛躍的に改善した。最新のツールでは、複雑怪奇な方程式を解くことによって停止性の証明を行うが、その実装は意外にもシンプルである。その秘訣は、複雑な問題を全て SAT 問題へ帰着させることにある。このチュートリアルでは、関数型言語などの計算モデルである項書換え系のための停止性検証ツールの実装方法を紹介する。「停止性ってなに？」「SAT ってなに？」という基礎からはじめ「どうやって停止性問題を SAT 問題に帰着させるか？」「なぜ SAT solver は速いのか」までを詳説する。

18:00-19:30 講師との歓談のためのレセプション（無料、赤ワインとチーズを少々準備しました） photo1 photo2

参加費

日本ソフトウェア科学会の会員非会員

学生１，０００円２，０００円

一般２，０００円４，０００円

当日会場で現金にてお支払いください。なるべくつり銭がないようご協力ください。（なお、非会員でも会員申し込み中の方は、会員の参加費額が適用されます。）

交通アクセス

交通アクセスをご参照ください。東京などから参加の場合、前日泊を考慮いただくことをお勧めいたします。

参加申込

レセプションなどの内容の確定のため、とりあえず8月31日で締め切りましたが、サマースクールへの参加自体は当日まで受け付けます。 ~~参加希望の方は、以下の情報を添えて、E-mailで ppl_ss07@jaist.ac.jp に事前にお知らせ頂けると助かります。~~

名前(ふりがな) : 
所属 : 
e-mail : 

一般・学生の別 : 一般・学生
日本ソフトウェア科学会会員 : 会員・非会員

その他の特別な希望があれば :

過去のサマースクール

問い合わせ先

サマースクール幹事
北陸先端科学技術大学院大学安心電子社会研究センター
小川瑞史

E-mail: mizuhito@jaist.ac.jp
Tel: 0761-51-1247, Fax 0761-51-1149

最終更新 2007.09.15

10:00-10:30	受付
10:30-12:30	非同期リアルタイム処理（デヴィットカトラーの見果てぬ夢）講師：小野諭（工学院大学） OHP photo1 photo2 概要：本講演では、並行性（Concurrency) をもつリアルタイム処理について、開発経験談を交えながら、記述モデル、デザインパターンなどをサーベイする。近年、シングルCPUのクロック上昇が行き詰まり、マルチコア化が進展している。また、Linux, Windows などの商用汎用（非実時間）OSは、こうしたハードウェアの特徴を生かすため、SMP（対称マルチプロセッサ）対応と、カーネルマルチスレッド化が積極的に行われている。本講演では、このような汎用OSに、SMP対応のリアルタイム機能拡張を行う手法について、機能要件、統一した記述モデル、典型的なデザインパターン、開発事例にもとづく留意事項などを説明する。記述モデルとしては、多重コンテキスト、非同期、非逐次化の３つを特徴とするオブジェクトモデルを用いる。このモデルは、SMPできわめて効率よく実装でき、また、高いスケーラビリティにより高多重度・高速ネットワーク処理が容易、さらに計算のキャンセルや電源障害などの非同期イベントの正確な制御が可能など、高性能・高信頼な実時間処理記述において、大きな利点を持っている。この記述モデルは、古く１９７０年代に開発された DEC社RSX-11, VAX/VMS などの実時間OS, 汎用OSにおいて、カーネル実装や実時間組み込みソフト記述に採用されたモデルである。その起源は、DECからMicrosoft に移り、WindowsNT の開発を指揮した David Cutler の発案に基づくものと考えられている。本講演では、こうした歴史的背景にさかのぼりながら、通常の Unix, POSIX API とは異なる本記述モデルの発展・受難と復活の流れについて、個人的見解を語る。
12:30-13:45	昼食・休憩（受付は 13:00-13:45開設、それ以降は会場の幹事・小川までお願いします）
13:45-15:45	Substructural Logics ---- 証明論的視点から講師：小野寛晰 (北陸先端科学技術大学院大学) OHP Related photo1 photo2 概要： Substructural logics (部分構造論理）の研究はこの２０年間ほどの間に大きな発展を遂げてきた。Substructural logics は Lambek 計算、relevant logics、linear logic、多値論理などの多くの代表的な非古典論理を含んでいるが、その基本的な体系の形式化にはシーケント計算が用いられている。それでは、シーケント計算を用いることがこれらの非古典論理の理解のためになにか本質的な意味を持つのだろうか？この講演では最近の substructural logics の研究成果をふまえ、この問いに対する一つの解答をあたえるとともに、シーケント計算による形式化の特質を改めて検討してみたい。（補足）講演では、技術的な内容よりも概念的な解説に重点を置くので、論理についての基本的な知識のみを仮定する。
16:00-18:00	停止性自動検証ツールにおける SAT Solver の使い方講師：広川直 (北陸先端科学技術大学院大学) OHP photo1 photo2 概要：項書換えや関数型言語のプログラムの停止性を自動証明するツールは、この5年間で証明能力・実行速度ともに飛躍的に改善した。最新のツールでは、複雑怪奇な方程式を解くことによって停止性の証明を行うが、その実装は意外にもシンプルである。その秘訣は、複雑な問題を全て SAT 問題へ帰着させることにある。このチュートリアルでは、関数型言語などの計算モデルである項書換え系のための停止性検証ツールの実装方法を紹介する。「停止性ってなに？」「SAT ってなに？」という基礎からはじめ「どうやって停止性問題を SAT 問題に帰着させるか？」「なぜ SAT solver は速いのか」までを詳説する。
18:00-19:30	講師との歓談のためのレセプション（無料、赤ワインとチーズを少々準備しました） photo1 photo2

	日本ソフトウェア科学会の会員	非会員
学生	１，０００円	２，０００円
一般	２，０００円	４，０００円