研究室紹介
- 一般向け紹介はこちら（英語）
- 教養課程学生向け，研究室紹介 .txt
- 研究室配属前の学部4年生向け，情報科学演習IIIの説明資料（下を見てね）
- 大学院修士課程受験者向け，研究室紹介 (ver. May 2014) .pdf
情報科学演習III
2011年度発足の（まだまだ）新しい研究室です．計算機科学のいろいろな側面に対して，抽象数学を使った数理モデルを作ることで，現象のよりよい理解と共に応用上の手法を得ることが目的です．たとえば，応用上の例は並行システム論・システム検証・関数型プログラミング言語・量子計算・ハイブリッドシステムなどで，使う数学は圏論 category theory や数理論理学などです．
情報科学演習IIIでは教科書や論文の輪講を通じて，このような研究アプローチの面白いところをかいま見てもらうと共に，共同研究における議論のスキルを身につけてもらおうと考えています． 輪講のテーマは受講者と相談してきめますが，以下に例を挙げます．
- 余代数による状態遷移システムの圏論的モデル
Jacobsの教科書(の草稿）をもとにして、オートマトンなどの状態遷移システムを圏論的に抽象化す る研究について学びます。 - 圏論の基礎
Crole または Leinster の教科書をもとにして，圏論に入門します． - 超準解析とハイブリッド・システム
Goldblatt の教科書をもとに超準解析を学び（論理学をたくさん使います）、ハイブリッド・システム （連続的な物理データとデジタルな離散的データを両方扱うようなシステム）の研究につなげます。 - 関数型言語の操作的意味論
次の文献のどちらか（どちらも？）を使って，関数型言語の操作的意味論に関する推論方法を学びます．
Andrew Pitts. Typed operational reasoning. In Benjamin C. Pierce, editor, Advanced Topics in Types and Programming Languages, chapter 7. MIT Press, 2005.
Pitts (in: Adv. Topics in Bisimulation and Coinduction, Sangiorgi & Rutten eds.) の Book Chapter - 様相論理とプロセスの等価性
Stirling (in: Adv. Topics in Bisimulation and Coinduction, Sangiorgi & Rutten eds.) の Book Chapterを もとにして，bisimilarity によるプロセス等価性の定義と，様相論理による特徴付け，さらに不動点論理について学びます． - 表示的意味論の基礎
Apt & Plotkin, J. ACM 1986 を読んで，domain theory の基本的な問題意識と テクニックについて学びます． - 確率的システムの検証手法
Baier & Katoen の教科書をもとに，確率的システムの検証アルゴリズムについて学びます．