学部・大学院区分
Undergraduate / Graduate		理学部
時間割コード
Registration Code		0619921
科目区分
Course Category		専門科目
Specialized Courses
科目名　【日本語】
Course Title		数理解析・計算機数学特別講義Ⅰ
科目名　【英語】
Course Title		Special Course on Computational Mathematics and Computer Science Ⅰ
コースナンバリングコード
Course Numbering Code
担当教員　【日本語】
Instructor		未定（理） ○
担当教員　【英語】
Instructor		 ○
単位数
Credits		1
開講期・開講時間帯
Term / Day / Period		秋集中 その他 その他
Intensive(Fall) Other Other
授業形態
Course style		講義
Lecture
学科・専攻
Department / Program
数理学科
必修・選択
Compulsory / Selected
選択


授業の目的　【日本語】
Goals of the Course(JPN)
プログラミング言語や仕様記述に関して重要である型理論について、その初歩を、数学的に厳密に説明する。
授業の目的　【英語】
Goals of the Course
Type theory gives a fundamental framework for programming languages and software specification. This course will introduce type theory and explain it in a mathematically rigorous way.
到達目標　【日本語】
Objectives of the Course(JPN))
(1) 型理論の初歩を数学的に厳密に理解すること。
(2) 型理論を実際の問題に応用できるようになること。
到達目標　【英語】
Objectives of the Course
(1) Complete mathematical understanding of the introductory part of type theory
(2) Ability of applying type theory to practical problems
授業の内容や構成
Course Content / Plan
(1) 1--4回: 型理論の基礎となる最も簡単な型理論である単純型理論λ→をいろいろな角度から説明する。λ→の定義を与える。型理論に対して一般に定義できる性質としてサブジェクトリダクション性、強正規化性、主型の存在についてλ→を例に用いて説明する。λ→に対するこれらの性質を証明する。
(2) 1,4回: プログラミング言語 ML の型理論について説明し、型推論のアルゴリズムを説明し、その正しさを証明する。
(3) 5--6回: 型理論 F を説明し、その強正規化性を証明する。
履修条件
Course Prerequisites
ラムダ計算の知識をもっていることが望ましい。
This course will be taught in Japanese.
関連する科目
Related Courses
なし
「履修取り下げ届」提出の要・不要
Necessity / Unnecessity to submit "Course Withdrawal Request Form"
要
履修取り下げの条件等
Conditions for Course Withdrawal
−
成績評価の方法と基準
Course Evaluation Method and Criteria
授業の達成目標の(1)(2)が習得できたかどうかをレポート(80%)および授業中の質問(20%)により判定する。
不可(F)と欠席(W)の基準
Criteria for "Fail (F)" & "Absent (W)" grades
総点60点以上を合格とする
参考書
Reference Book
[1] 龍田 真， 型理論 (近代科学社， 1992.11).
[2] S. Abramsky， Dov M. Gabbay and T. S. E. Maibaum， ”Handbook of logic in computer science” (Oxford University Press， 1992)， Page 117--309.
教科書・テキスト
Textbook
なし
課外学習等（授業時間外学習の指示）
Study Load(Self-directed Learning Outside Course Hours)
なし
注意事項
Notice for Students
−
他学科聴講の可否
Propriety of Other department student's attendance
可
他学科聴講の条件
Conditions for Other department student's attendance
高度な数学的推論能力が必要。
レベル
Level
1
キーワード
Keyword
型理論、ラムダ計算
type theory, lambda-calculus
履修の際のアドバイス
Advice
−
授業開講形態等
Lecture format, etc.
対面
遠隔授業（オンデマンド型）で行う場合の追加措置
Additional measures for remote class (on-demand class)
−