型付きラムダ計算
これを論理学的に見れば、二階述語論理に属する全ての関数を記述できることを意味する。依存型のあるラムダ計算は直観主義的型理論の基盤であり、calculus of constructions や logical framework (LF) の基盤である。Berardi の成果に基づき Barendregt が提案したラムダ・キューブは、純粋な型付きラムダ計算(単純型付きラムダ計算、System F、LF、calculus of constructions など)の関係を体系化したものである。
一部の型付きラムダ計算には「サブタイピング」の概念が導入されている。すなわち、 A {\displaystyle A} が B {\displaystyle B} のサブタイプ(下位型)であるとき、 A {\displaystyle A} 型の項は必ず B {\displaystyle B} 型の項でもある。サブタイピングのある型付きラムダ計算としては、単純型付きラムダ計算に conjunctive type を加えたものと System F-sub(英語版) (F<:) が挙げられる。
以上の体系はすべて(型のないラムダ計算以外)、「強く正規化 (strongly normalizing)」する。すなわち、全ての計算は停止する。結果としてそれらは論理として一貫しており、uninhabited types がある。しかし、強く正規化しない型付きラムダ計算も存在する。