ラムダ計算
計算の形式モデル。1930年代にアロンゾ・チャーチが考案した。規則は変数、抽象（λx.本体）、適用（f x）の三つだけで、チューリング完全であり、コンピュータで計算できるものは何でも計算できる。
関数型プログラミングの土台である。カリー化（引数一つの関数が別の関数を返すこと）の名は、ハスケル・カリーに由来する。Yコンビネータを使えば、名前のない関数で再帰を実現できる。型付きラムダ計算（単純型付き→System F→構成の計算）はHaskell、ML、Coq、Agda、Leanへつながった。関数型プログラミングは、その直系の子孫と言える。チャーチ＝チューリングのテーゼによれば、ラムダ計算とチューリングマシンは同じ計算能力のクラスを表現する。