授業の目的 【日本語】
Goals of the Course(JPN) | | | ソフトウェア検証の厳密化や自動化のためには，プログラミング言語を形式的に理解することが必須である．この講義ではプログラミング言語の性質を形式的に捉える手法の一つとして，型システムの理論と，その検証技術への応用について理解することを目的とする． |
|
|
授業の目的 【英語】
Goals of the Course | | | We learn the theory of the lambda calculus, a model of functional programming languages, and the type systems of the lambda calculus for program verification. |
|
|
到達目標 【日本語】
Objectives of the Course(JPN) | | | 受講者は授業終了時に以下の知識を身に付けている：ラムダ計算の理論，型付ラムダ計算の性質とプログラム検証への応用手法． |
|
|
到達目標 【英語】
Objectives of the Course | | |
|
授業の内容や構成
Course Content / Plan | | プログラミング言語特論1に続き，プログラミング言語およびプログラムの意味を厳密に捉え，解析する手法について学ぶ．とくに，型の概念を用いたプログラムの解析手法について，理論と応用の両面から解説する。理論面では，数理論理学的な概念を基礎とした型システムの定義やその性質を学ぶ。 応用面では，型システムを利用したプログラム検証の技術について学ぶ．
〔計画〕
1. ガイダンス
2. ラムダ計算
3. 単純型付ラムダ計算
4. 型健全性
5. 直観主義論理とカリーハワード同型
6. 多相型システムとMLの型推論 | |
|
|
履修条件・関連する科目
Course Prerequisites and Related Courses | | | 情報学部科目の論理学1, 2c，および，プログラミング言語特論1を受講していることが望ましい． | |
|
|
成績評価の方法と基準
Course Evaluation Method and Criteria | | | 数回のレポート課題の評価50%，期末の筆記試験50%，合計100点満点で60点以上を合格とする．ただし，大学の授業実施方針の状況によっては，期末の筆記試験に代えてレポートによる評価を行なうことがある | |
|
|
教科書・参考書
Textbook/Reference book | | 参考書：B.C. Pierce「型システム入門 プログラミング言語と型の理論」（オーム社）
（もしくは原著 B.C. Pierce "Types and Programming Languages" (MIT Press）
その他，必要に応じて資料を配布する。 | |
|
|
課外学習等（授業時間外学習の指示）
Study Load(Self-directed Learning Outside Course Hours) | | | 各回の授業内容を復習し，レポート課題を提出すること． | |
|
|
授業開講形態等
Lecture format, etc. | | |
|
遠隔授業（オンデマンド型）で行う場合の追加措置
Additional measures for remote class (on-demand class) | | |
|