学部・大学院区分

多・博前

時間割コード

3213176

科目区分

Ｃ類（実習）
Category C

科目名　【日本語】

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

科目名　【英語】

Practical Class on Computational Mathmatics and Computer Science 4

コースナンバリングコード

担当教員　【日本語】

GARRIGUE JACQUES ○

担当教員　【英語】

GARRIGUE JACQUES ○

単位数

開講期・開講時間帯

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

授業形態

学科・専攻

多元数理科学研究科

必修・選択

授業の目的　【日本語】

テーマ：プログラムの意味論・型と論理

プログラミング言語は貪欲に機能を増やしていくが、ラムダ計算がそれらの機能を統一的に扱えるため、中心的な役割を得た。しかし、ラムダ計算の等式理論が比較的容易に定義できるものの、より抽象的な表示的意味論の構築が集合論の枠組みに中々収まらない。
この少人数クラスでは型なしラムダ計算および様々な型付ラムダ計算のモデルを作る方法を見ていく。圏論と領域論が具体的な枠組みを与え、そのモデルが新しいプログラムの構成法につながる。Haskellでよく使われるモナドなどがそのモデル化から生まれたものである。

具体的には、AmadioとCurienの「Domains and lambda calculi」を読んでそれを勉強する予定である。また、必要に応じて他の文献も見ていく。

Theme: Programming language semantics, types and logic

Programming languages have many functionalities. The lambda-calculus acquired its central role due to its ability of handling them in a uniform way. Yet, while the equational theory of lambda-calculus is relatively easy to define, the construction of a more abstract denotational semantics does not fit easily into the framework of set
theory.
In this small class we will study the construction of models for the untyped and typed lambda-calculus. Category theory and domain theory provide a concrete way to build models, and offer insights into programming languages. The use of monads in the language Haskell is an example of a programming construct derived from categorical models.

授業の目的　【英語】

到達目標　【日本語】

* ラムダ計算と型理論の基礎を習う．
* モデル構築に必要な圏論の概念を習う．
* ラムダ計算に対する具体的なモデルの構築法を習う．

到達目標　【英語】

授業の内容や構成

基本的には本や論文の輪講という形を取る．ほとんどの資料が英語になるので，発表する人がちゃんと下調べをして，少くとも言葉が皆に理解できるように説明していただく．後期になると，個人の希望に応じて，一人で論文を読んで，報告するという形でもよい．

この少人数クラスのカリキュラムは1年間で完結するが，次の年の少人数クラスは計算と論理への少し異ったアプローチにしようと考えているので，同じ分野で続けることができる．

This course is mainly a reading seminar. The participants are expected to prepare carefuly the parts they are assigned, in order to give explanatory presentations. During the second semester, participants may also read individually chosen articles and report on them.
This course has contents for one year, but it is expected that another small class tackling logic and computation from a different point of view will be held during the next year, so that participants may complete their knowledge of this subject.

履修条件

特に何も求めていない．論理学やプログラミングの知識が少しあると楽になる．

This course basically uses Japanese as communication language.
Contact the teacher if you would like to participate in English.