学部後期課程
HOME 学部後期課程 計算機言語論
戻る
学内のオンライン授業の情報漏洩防止のため，URLやアカウント、教室の記載は削除しております。
最終更新日：2024年10月18日

授業計画や教室は変更となる可能性があるため、必ずUTASで最新の情報を確認して下さい。
UTASにアクセスできない方は、担当教員または部局教務へお問い合わせ下さい。

計算機言語論

プログラムの自動検証の理論について講義を行う．特に，高階モデル検査という発展的話題を通して，形式言語理論やプログラミング言語理論がプログラム検証にどう応用されるのかの理解することを目標とする．
MIMA Search
時間割／共通科目コード
コース名
教員
学期
時限
0510083
FSC-IS4083L1
計算機言語論
小林　直樹
S1
月曜3限
マイリストに追加
マイリストから削除
講義使用言語
日本語
単位
1
実務経験のある教員による授業科目
NO
他学部履修
可
開講所属
理学部
授業計画
1. 導入：高階モデル検査についての概観 2. 高階文法と高階プッシュダウンオートマトン（無限木の生成系として） 3. 無限木オートマトン（無限木の性質記述方法として） 4. 様相論理（無限木の性質記述方法として） 5. 高階モデル検査のための型システム 6. 高階モデル検査アルゴリズム 7. プログラム検証への応用
授業の方法
初回のみオンライン、以降は対面での実施を予定
成績評価方法
主にレポート課題による．
教科書
なし
参考書
講義中に指定する
履修上の注意
この科目は理学部情報科学科の４年生の科目であり、理学部情報科学科の３年生は履修登録できない。 4学期の「形式言語理論」で習うオートマトンや生成文法、および3年Aセメの「言語モデル論」で習うλ計算、型システムについての知識を前提とする。 次の講義までにスライド等で前回の講義内容を確認するとともにレポート課題に取り組むこと。
戻る