言語モデル論(2023年度Aセメスター)

• 担当教員：小林直樹
• 講義日：月曜2限（10:25-12:10）
• 場所：理学部7号館007講義室（一部オンラインで実施する場合があるので、ITC-LMS上のアナウンスに注意すること）
• 質問等の連絡先：
• 期末試験：2024年1月29日(月) 10:25-12:10 @ 理学部１号館285講義室
• 講義関連資料（すべて再配布禁止。パスワードは講義中に伝えます。）
  • スライド（閲覧のためのパスワードは初回講義時にアナウンス）
    • 構文
    • 操作的意味論
    • プログラムの性質に関する推論
    • ホーア論理
    • ホーア論理2（最弱事前条件とホーア論理の相対完全性）
    • 表示的意味論
    • λ計算1（代入と簡約）
    • λ計算2（表現能力、チャーチ・ロッサー性、簡約戦略）
    • 型つきλ計算
    • 型つきλ計算2（型推論と多相型システム）
    • 型システムに関するその他の話題、オブジェクト指向言語
    • 論理プログラミング，並行計算のモデル
  • 教科書： 小林直樹、住井英二郎、プログラム意味論の基礎、サイエンス社、ISBN 978-4-7819-1483-1. 正誤表
  • 参考書：
    • 徳山、小林（編集）、理論計算機科学事典，朝倉書店、6章から８章．
    • 前半部分（while言語の意味論)

      Glynn Winskel, The Formal Semantics of Programming Languages: An Introduction, MIT Press.

    • 後半部分（ラムダ計算と型システム）

      萩谷昌己、西崎真也、論理と計算のしくみ、第5章、岩波書店.

      高橋正子、計算論：計算の可能性とラムダ計算、近代科学社.

      H. P. Barendregt, The Lambda Calculus, its Syntax and Semantics, North Holland, ISBN 0444875085.

• レポートについて

  課題はITC-LMSに掲示し，提出も原則としてITC-LMS経由とします．

  他人のものを写したものを提出する等の不正が見つかった場合には，試験の際のカンニングに準じて，厳罰を適用します． こちらのページのレポートに関する注意も確認すること．