学部・大学院区分
Undergraduate / Graduate

多・博前

時間割コード
Registration Code

3211135

科目区分
Course Category

Ａ類Ⅲ（集中講義）
Category A-3

科目名　【日本語】
Course Title

数理解析・計算機数学特別講義Ⅰ

科目名　【英語】
Course Title

Special Course on Computational Mathematics and Computer ScienceⅠ

コースナンバリングコード
Course Numbering Code

担当教員　【日本語】
Instructor

龍田真 ○

担当教員　【英語】
Instructor

TATSUTA Makoto ○

単位数
Credits

開講期・開講時間帯
Term / Day / Period

秋集中その他その他
Intensive(Fall) Other Other

授業形態
Course style

学科・専攻
Department / Program

多元数理科学研究科

必修・選択
Required / 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 を説明し、その強正規化性を証明する。

(1) 1--4 classes: Simply typed lambda calculus will be explained in several aspects. Its definition， subject reduction property， strong normalizability， existence of principal types will be explained. These properties for simply typed lambda calculus will be proved.
(2) 1,4 classes: Type inference in programming language ML will be explained. Its algorithm will be given and its correctness will be proved.
(3) 5--6 classes: Type theory F will be explained and its strong normalizability will be proved.

履修条件
Course Prerequisites

ラムダ計算の知識をもっていることが望ましい。
This course will be taught in Japanese.