計算機言語論（2026年度S1）

• 小林直樹
• 講義日：月曜3限（13:00-14:45）.
• 場所: 理学部1号館341講義室
• 参考資料・文献
  • 徳山 豪、小林直樹編集、理論計算機科学事典、朝倉書店（第5章および8.1節）
  • E. Gradel et al., ed., " Automata, Logics, and Infinite Games: A Guide to Current Research", Springer LNCS 2500, ISBN 3-540-00388-6, 2002.

    無限語/木に関するオートマトン、論理、ゲームに関するチュートリアル論文集

  • Wolfgang Thomas, "Languages, automata, and logic", Handbook of formal languages, vol. 3, pp.389 - 455 .

    無限語/木に関するオートマトンと論理（著者のホームページからdraftをダウンロード可能）

  • N. Kobayashi, "Higher-Order Model Checking: From Theory to Practice", LICS 2011.

    高階モデル検査関連の文献へのポインタとして

  • N. Kobayashi, "Model Checking Higher-Order Programs", Journal of the ACM, 60(3), 2013.

    高階モデル検査アルゴリズムとプログラム検証への応用について

  • Arnaud Carayol and Olivier Serre, Higher-order recursion schemes and their automata models, a chapter of Handbook of Automata Theory, 2021

    HORSに関する歴史的経緯など(3節以降のCPDAとの関係は難解なので専門家向き)。

• 質問、レポートの提出先（メールの場合）：
• 講義関連資料（再配布禁止。パスワードは講義中に伝えます）
  • スライド
    • 導入
    • 木生成系
    • 木オートマトン
    • 高階モデル検査のための型システムとアルゴリズム
    • 高階モデル検査のプログラム検証への応用
    • 高階モデル検査のデータ圧縮への応用
• レポート課題: UTOL(UTokyo LMS)に掲示
• レポートについて
  • 提出は、原則、UTOLで行うものとします． やむをえずメールで提出する場合、その理由を明記するとともに、 Subjectに、「計算機言語論第○回レポート」と書き、本文の冒頭に学籍番号、氏名を記入してください。
  • 他人のものを写したものを提出する等の不正が見つかった場合には，試験の際のカンニングに準じて，厳罰を適用します． こちらのページのレポートに関する注意も確認すること．