大学院
過去（2021年度）の授業の情報です
学内のオンライン授業の情報漏洩防止のため，URLやアカウント、教室の記載は削除しております。
最終更新日：2024年4月1日
授業計画や教室は変更となる可能性があるため、必ずUTASで最新の情報を確認して下さい。
UTASにアクセスできない方は、担当教員または部局教務へお問い合わせ下さい。
最終更新日：2024年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. 並行計算やプログラム等価性に関するその他の話題
授業の方法
オンライン講義の予定
成績評価方法
レポートによる。
教科書
特になし
参考書
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
履修上の注意
プログラミング言語の基礎（構文および操作的意味）、情報論理学についての知識を仮定する。
