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