Curry-Howard同型対応
最も一般的には，
単純型付きλ計算
の型
直観主義論理
の論理式
が対応していることを指す
#型理論
Haskell Curry
と
Wiliam A. Howard
に帰する．