型理論 - Skype数学勉強会

日時

毎週月曜日

20:45~22:15

テキスト

『型システム入門 プログラミング言語と型の理論』 - Benjamin C. Pierce (著), 住井 英二郎 (監訳), 他7名

原著: Types and Programming Language (TaPL)

前提知識

• 論理学
• 数学(集合, 離散数学)
• 関数型プログラミング言語(Scheme, OCaml, Haskell ...)
• コンパイラの基礎的な概念(抽象構文, BNF文法, 評価, 抽象機械 ...)

などが前提知識としてあるとベストですが、無くてもどうにかなると思われます

型理論概説

型理論とは元々素朴集合論におけるラッセルのパラドクスに対する理論としてラッセル自身が構築したものになります。また、公理的集合論に似ていることも示されています。

その顕著な応用例としてはコンピュータプログラミングが挙げられます。型によるエラー検出や安全性向上の効果は十分期待できるものです。

今回使用するテキストは型システムをOCamlというプログラミング言語を利用して実装し、学習していく構成になっています。

応用を挙げれば幾らでもあり、この勉強会はかなり深い話への導入にあります

備考

• 聴講可能
• 現在メンバー募集中
• Haskell勉強会と少なからず関係があります
• 3章→5章→8章→9章→11章の順に進める予定です(プログラム要素は少なめに理論を追う形で進めます)

活動報告

1. 2015/09/07 演習3.2.5まで whiteboard
2. 2015/09/14 補題3.3.3まで whiteboard1 whiteboard2
3. 2015/09/28 定義3.5.3まで whiteboard
4. 2015/10/19 演習3.5.10まで whiteboard
5. 2015/11/02 定理3.5.12まで whiteboard

次回予告

11/23 20:45 ~ 22:15 p.29 演習3.5.13より