大学院
学内のオンライン授業の情報漏洩防止のため，URLやアカウント、教室の記載は削除しております。
最終更新日：2025年4月1日
授業計画や教室は変更となる可能性があるため、必ずUTASで最新の情報を確認して下さい。
UTASにアクセスできない方は、担当教員または部局教務へお問い合わせ下さい。
最終更新日：2025年4月1日
授業計画や教室は変更となる可能性があるため、必ずUTASで最新の情報を確認して下さい。
UTASにアクセスできない方は、担当教員または部局教務へお問い合わせ下さい。
計算機言語システム論
計算機言語システム論
計算モデル、型システムなどのプログラミング言語の基礎理論と、その言語処理系、プログラム検証などへの応用について、最新のトピックを交えながら解説する。今年度は特に、並行計算モデルに焦点を当て、並行計算の代表的なモデルであるCCS、π計算をとりあげ、操作的意味、仕様記述のための様相論理、検証手法（双模倣、モデル検査、型システム）、セキュリティプロトコルへの応用などについて概説する。
時間割／共通科目コード
コース名
教員
学期
時限
4810-1109
GIF-CS5009L1
計算機言語システム論
小林 直樹
火曜3限
マイリストに追加
マイリストから削除
講義使用言語
日本語
単位
2
実務経験のある教員による授業科目
NO
他学部履修
可
開講所属
情報理工学系研究科
授業計画
1. 導入
2. 並行計算モデル(CCS) I
3. 並行計算モデル(CCS) II
4. プロセス等価性I: トレース等価性、強双模倣
5. プロセス等価性II: 観測等価性
6. 様相論理
7. モデル検査
8. π計算I: 構文と操作的意味
9. π計算II: プロセス等価性
10. 並行計算の型システム
11. spi計算とセキュリティプロトコル
12. プロトコル検証
13. 並行計算やプログラム等価性に関するその他の話題
授業の方法
スライド（英語）を用いて講義を行う。
原則として対面で実施予定。
The slides are written in English. The lecture may also be given in English, depending on students' preference.
成績評価方法
レポートによる。
教科書
特になし
参考書
R. Milner, Communication and Concurrency, Prentice Hall, 1989
R. Milner, Communicating and Mobile Systems: the p-calculus, Cambridge University Press, 1999
D. Sangiorgi and D. Walker, The p-calculus: A Theory of Mobile Processes, Cambridge University Press, 2001
C. Stirling, Modal and Temporal Properties of Processes, Springer, 2001
履修上の注意
プログラミング言語の基礎（構文および操作的意味）、情報論理学についての知識を仮定する。
