パンの木を植えて

主として数学の話をするブログ

型理論の資料,リソース

\[ %%% 黒板太字 %%% \newcommand{\A}{\mathbb{A}} %アフィン空間 \newcommand{\C}{\mathbb{C}} %複素数 \newcommand{\F}{\mathbb{F}} %有限体 \newcommand{\N}{\mathbb{N}} %自然数 \newcommand{\Q}{\mathbb{Q}} %有理数 \newcommand{\R}{\mathbb{R}} %実数 \newcommand{\Z}{\mathbb{Z}} %整数 %%% 2項演算 %%% \newcommand{\f}[2]{ \frac{#1}{#2} } \]

最近,型理論のことを勉強したいと思っています.

lean 関連の文書の翻訳をするにあたり,型付ラムダ計算のことも知らないド素人のままではまずいだろうという考えです.詳しい人にレビューしてもらえるから大丈夫,ではなくて自分がある程度詳しくなるべきだと思いました.

人に訊いたり検索したりして探しましたので,以下にメモしておきます.なお関連がありそうなものを手当たり次第に放り込んでいるので,関係がないものが含まれる可能性があります.

Road Map
Notes
Videos
Books
プログラム意味論

ひとに教えてもらった本.

Types and Programming Languages

TaPL の略称で有名な本です.

型システム入門 プログラミング言語と型の理論

上記の和訳です.


探せばまだあると思いますが,とりあえずこのあたりで.