「型の理論」入門

概要

「型の理論」は、数学・論理学・計算機科学の三つの領域を結びつける重要な役割を担っています。このショート・ムービーでは、「型の理論」の発展の各トピックを、紹介しています。こちらの資料 の第二部に対応しています。

目次

1. 「型のないラムダ計算1」 (movie, スライド)
2. 「型のないラムダ計算2」 (movie, スライド)
3. 「型付きラムダ計算」 (スライド)
4. 「論理的推論1 — 判断と論理式」 (movie, スライド)
5. 「論理的推論2 — Natural Deduction」 (movie, スライド)
6. 「Curry-Howard対応1」 (movie, スライド)
7. 「Curry-Howard対応2 –「型」と「証明」」 (movie, スライド)
8. 「Dependent Type Theory」 (movie, スライド)
9. 「Homotopy Type Theory」 (movie, スライド)

1. 「型のないラムダ計算1」 (スライド)

2. 「型のないラムダ計算2」 (スライド)

3. 「型付きラムダ計算」 (スライド)

4. 「論理的推論1 — 判断と論理式」 (スライド)

5. 「論理的推論2 — Natural Deduction」 (スライド)

6. 「Curry-Howard対応1」 (スライド)

7. 「Curry-Howard対応2 –「型」と「証明」」 (pdf)
(スライド)

8. 「Dependent Type Theory」 (スライド)

9. 「Homotopy Type Theory」 (スライド)