Simply typed lambda calculus

The foundational typed lambda calculus where each Lambda abstraction explicitly annotates its parameter with a type, providing a basis for more advanced type systems while guaranteeing termination.