学部・大学院区分
Undergraduate / Graduate
情報・博前
時間割コード
Registration Code
2550048
科目区分
Course Category
主専攻科目
科目名 【日本語】
Course Title
プログラミング言語特論2
科目名 【英語】
Course Title
Programming Language Theory 2
コースナンバリングコード
Course Numbering Code
GSI156040J
担当教員 【日本語】
Instructor
中澤 巧爾 ○
担当教員 【英語】
Instructor
NAKAZAWA Koji ○
単位数
Credits
1
開講期・開講時間帯
Term / Day / Period
春2期 火曜日 2時限
Spring2 Tue 2
対象学年
Year
1年
1
授業形態
Course style

開講系(学部)・開講専攻(大学院)
Subject
情報システム学専攻
必修・選択
Required / Selected
選択


授業の目的 【日本語】
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)