SAKAI Masahiro - 型理論F Diff

  • Added parts are displayed like this.
  • Deleted parts are displayed like this.

= 型理論F

Giraldによって構成された((<型理論>))

((<λ-cube>))では((<λ2>))と呼ばれる

((<Curry-Howard の同型対応>))によって、((<2階命題論理>))に対応する。