ラムダキューブ

• 上: パラメトリック多相
• 奥: 型オペレータ
• 右: 依存型

すべて取り入れたのが Calculus of Constructions

• Simply Typed Lambda Calculus

  • 一階命題論理に対応

• λ2

  • パラメトリック多相
  • 二階命題論理

• Calculus of Constructions

  • 高階述語論理