学部・大学院区分
Undergraduate / Graduate

多・博前

時間割コード
Registration Code

3213173

科目区分
Course Category

Ｃ類（実習）
Category C

科目名　【日本語】
Course Title

数理解析・計算機数学実習１

科目名　【英語】
Course Title

Practical Class on Computational Mathmatics and Computer Science 1

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

担当教員　【日本語】
Instructor

GARRIGUE JACQUES ○

担当教員　【英語】
Instructor

GARRIGUE JACQUES ○

単位数
Credits

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

春集中その他その他
Intensive(Spring) Other Other

授業形態
Course style

学科・専攻
Department / Program

多元数理科学研究科

必修・選択
Required / Selected

選択必修

授業の目的　【日本語】
Goals of the Course(JPN)

テーマ：型理論と数学を結ぶホモトピー型理論
型理論と論理の関係は古くから知られている。しかし、型理論において、等式の証明の意味が課題であった。 VoevodskyとWarrenが提案したホモトピー型理論では、等価性に新しい解釈を与えることで、この課題を進展させた。
この少人数クラスでは型理論と論理の関係、特に位相空間での解釈を基礎から学ぶ。また、口頭発表および自律的な研究習慣のスキルの獲得も目指す。

授業の目的　【英語】
Goals of the Course

Theme: Connecting Type Theory and Mathematics through Homotopy Type Theory
The correspondance between type theory and logic is now well known. However, the meaning of equality proofs was unclear. Homotopy type theory, which was proposed separately by V. Voevodsky and M. Warren, advanced our understanding by providing a new interprestation of equality inside type theory.
In this course, we will learn from the ground on the connection between type theory and logic, and particularly their interpretation in topological spaces. It also enhances the development of students' skill in making oral presentation and self-regulated studying.

到達目標　【日本語】
Objectives of the Course(JPN))

以下を目標としている
* λ計算および型体系の概念を理解する
* 論理との関係を理解する
* ホモトピー型理論の基本的な概念を理解する
* 帰納的な定義に関する証明方法をマスターする
* 要点をまとめて定義・証明を説明する技術を磨く

到達目標　【英語】
Objectives of the Course

This cours has the following goals
* Understand lambda-calculus and the concept of type system
* Understand its connection to logic
* Understand the fundamental concepts of Homotopy Type Theory
* Master proofs by induction in various systems
* Improve one's presentation skills, describing definitions and proofs in a clear way

授業の内容や構成
Course Content / Plan

基本的には本や論文の輪講という形を取る．ほとんどの資料が英語になるので，発表する人がちゃんと下調べをして，少くとも言葉が皆に理解できるように説明していただく．後期になると，個人の希望に応じて，一人で論文を読んで，報告するという形でもよい．
この少人数クラスのカリキュラムは1年間で完結するが，次の年の少人数クラスは計算と論理への少し異ったアプローチにしようと考えているので，同じ分野で続けることができる．

In this course students usually present part of a book or article, either the main course material, or and article of their choice. The main course material is intended for one year, but connected subjects will be available in the following years.

履修条件
Course Prerequisites

希望提出前に担当教員と連絡をとること．
The students should communicate with the instructor before application.
使用言語は応相談．
Language will be decided after a discussion with the students.