依存型理論
依存型理論(dependent type theory; DTT)
Per Martin-Löf
が
Martin-Löf型理論
(MLTT)として出してきた？
直観主義型理論
(intuitionistic type theory)
Coq
、
Agda
、
Lean
などの基盤となる型理論になっている
具体的な記法は
Martin-Löf型理論
の方に寄せる
Martin-Löf型理論の記法など
型理論、依存型理論を学習する
関連
Homotopy Type Theory(HoTT)
帰納的型
カリー＝ハワード対応
カリー／ハワード／ランベック対応
Homotopy Type Theory(HoTT)
Propositions as Types
ホモトピー型理論と論理・集合・圏論など？の関係
参考
『［2021CAPE公開セミナー］ 論理学上級 Ⅱ-3「証明論的意味論としてのマーティン・レーフの構成的型理論」』
メモ
intensional type theory in nLab
『Homotopy Type Theory 入門』
DependentType.pdf - Google ドライブ
『Homotopy Type Theory: Univalent Foundations of Mathematics』
Martin-Löf dependent type theory in nLab
従属型理論の登場 - YouTube
依存型理論をどうやって学べばいいか
The best coarse of study for learning dependent types? : haskell
『依存型を含むマルチステージプログラミングの型理論』
https://youtu.be/RPIPLXeQqXk?si=QK0ExG8mXRjw7898
Programming in Martin-Löf’s Type Theory
Martin-Löf型理論(MTT)
https://youtu.be/WSVXbNw7IxQ?si=4g6DLgh3mO2Qh8zl
pdf:
https://drive.google.com/file/d/15l6xM-eCcfjbMq_qTUMC2oXV0DHiMmeZ/view
#型理論