依存型理論
#Fleeting_Notes
依存型理論(dependent type theory)
依存積型(パイ型)
$ \prod
依存和型(シグマ型)
$ \sum
帰納的型
カリー=ハワード同型対応
Martin-Löf型理論
参考
『[2021CAPE公開セミナー]論理学上級 Ⅱ-3 証明論的意味論としてのマーティン・レーフの構成的型理論』
関連
『依存型を含むマルチステージプログラミングの型理論』
単純型理論
Homotopy Type Theory(HoTT)
メモ
依存型 - Wikipedia
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
#型理論