型付きラムダ計算
型付きラムダ計算(かたつきラムダけいさん、英: typed lambda calculus)
ラムダ計算
で型がついているもの
単純型付きラムダ計算
デカルト閉圏(CCC)
関連
サブタイピング
ラムダ・キューブ
依存型理論
メモ
A Tutorial Implementation of a Dependently Typed Lambda Calculus