Typing Untyped Lambda-Terms, or Reducibility Strikes Again!

. It was observed by Curry that when (untyped) -terms can be assigned types, for example, simple types, these terms have nice properties (for example, they are strongly normalizing) . Coppo, Dezani, and Veneri, introduced type systems using conjunctive types, and showed that several important classes of (untyped) terms can be characterized according to the shape of the types that can be assigned to these terms. For example, the strongly normalizable terms, the normalizable terms, and the terms having head-normal forms, can be characterized in some systems D and D \Omega\Gamma The proofs use variants of the method of reducibility. In this paper, we present a uniform approach for proving several meta-theorems relating properties of -terms and their typability in the systems D and D Our proofs use a new and more modular version of the reducibility method. As an application of our metatheorems, we show how the characterizations obtained by Coppo, Dezani, Veneri, and Pottinger, can be easi..