SAKAI Masahiro - 型理論F Diff
- Added parts are displayed like this.
- Deleted parts are displayed
like this.
= 型理論F
Giraldによって構成された((<型理論>))
((<λ-cube>))では((<λ2>))と呼ばれる
((<Curry-Howard の同型対応>))によって、((<2階命題論理>))に対応する。
Giraldによって構成された((<型理論>))
((<λ-cube>))では((<λ2>))と呼ばれる
((<Curry-Howard の同型対応>))によって、((<2階命題論理>))に対応する。