Reducibility method in simply typed lambda calculus
Silvia Ghilezan, Viktor Kunčak
A general reducibility method for proving reduction properties of the simply typed lambda calculus is presented and sufficient conditions for its application are derived.