In this paper we introduce Curryfied Term Rewriting Systems, and a notion of partial type assignment on terms and rewrite rules that uses intersection types with sorts and omega. Three operations on types -- substitution, expansion, and lifting -- are used to define type assignment, and are proved to be sound. With this result the system is proved closed for reduction. Using a more liberal approach to recursion, we define a general scheme for recursive definitions and prove that, for all systems that satisfy this scheme, every term typeable without using the type-constant omega is strongly normalizable. We also show that, under certain restrictions, all typeable terms have a (weak) head-normal form, and that terms whose type does not contain omega are normalizable.
