Lambda calculus

A minimal formal system for expressing computation using only variable binding and function application, yet serves as a foundation that can be extended with types, effects, recursion primitives, and other constructs to form the basis of modern programming languages.