型理論、依存型理論を学習する
型理論
、
依存型理論
を学ぶには
関連ページ:
型理論の文献
龍田 真
.
型理論I
. 1991
龍田 真.
型理論II
. 1991
龍田 真.
型理論III
. 1991
龍田 真.
型理論IV
. 1991
水上 達夫. 数学基礎論特論 (コンピュータ特別講義 I) 講師 龍田 真. 2001-11-01.
http://www.yl.is.s.u-tokyo.ac.jp/~tatsuo/types/types20011101.pdf
A Tutorial Implementation of a Dependently Typed Lambda Calculus
単純型付きラムダ計算
Martin-Löf’s型理論(MLTT)、直観的型理論(intensional type theory)
『Intuitionistic Type Theory』
. 1988
『Programming in Martin-Löf ’s type theory』
. 1990
『Intuitionistic Type Theory』Stanford Encyclopedia of Philosophy
(Webのやつ)
intensional type theory in nLab
関連しそうなもの
『Constructive Mathematics』
『型システム入門 －プログラミング言語と型の理論－』
(原著:
『Types and Programming Languages』
)
type theory in nLab
日本語文献
型システムのしくみ ― TypeScriptで実装しながら学ぶ型とプログラミング言語 – 技術書出版と販売のラムダノート
『型システム入門 －プログラミング言語と型の理論－』
CAPE公開セミナー
『［2021CAPE公開セミナー］ 論理学上級 Ⅱ-2「カリー・ハワード対応と『証明のデータ型としての命題』観」』
『［2021CAPE公開セミナー］ 論理学上級 Ⅱ-3「証明論的意味論としてのマーティン・レーフの構成的型理論」』
『新装版 プログラミング言語の基礎理論』
大堀淳の計算機科学チャネル - YouTube
Tatsuta Entrance
計算機科学のための圏論の基礎の基礎
自分のメモページ:
『計算機科学のための 圏論の基礎の基礎』
ホモトピー型理論
Homotopy Type Theoryの参考文献
『Homotopy Type Theory: Univalent Foundations of Mathematics』
『Introduction to Homotopy Type Theory』
の
未検証
Type-Driven Development with Idris
参考
型理論の資料，リソース - パンの木を植えて
Good introductory book to type theory? - MathOverflow
#型システム