１つ目の顔：「計算モデルとしてのラムダ計算」

ラムダ計算には単純かつ強力な計算規則（β簡約）が備わっており、 ラムダ計算の要素（ラムダ項）は、そのままプログラムとみなして 実行することが可能です。

２つ目の顔：「証明の理論としてのラムダ計算」

型付きラムダ計算のデータ型を論理式、ラムダ項を証明と捉える ことにより、ラムダ計算を、形式的な論理体系とみなすことが 出来ます。

３つ目の顔：「代数系としてのラムダ計算」

単純型付きラムダ計算（とそのモデル）は、自然に、カルテジアン 閉圏（Cartesian closed category）と呼ばれる圏論的な構造を 定めます。

１つ目の顔と２つ目の顔を組み合わせることにより、計算の世界と 論理の世界の深い結び付きが明らかにされてきました（Curry-Howard 対応）。２つ目と３つ目の顔は圏論的論理・圏論的型理論の分野で 基本的な役割を果たします。最後に、１つ目と３つ目の顔の関係は、 プログラミング言語の意味論（semantics of programming languages） と呼ばれる研究分野の骨子をなすものです。