 Untyped lambda calculus

The untyped lambda calculus forms terms from variables, abstraction, and application without assigning types.