This post describes the semantics of the lambda calculus.

This post examines a notion of equivalence for terms of the lambda calculus known as applicative bisimilarity.