Strong Normalization with Non-structural Subtyping

We study a type system with a notion of subtyping that involves a largest type ?, a smallest type ?, atomic coercions between base types, and the usual ordering of function types. We prove that any -term typable in this system is strongly normalizing; this solves an open problem of Thatte. We also prove that the fragment without ? types strictly fewer terms. This demonstrates that ? adds power to a type system. 1 Introduction Statically-typed languages are desirable for many reasons, but they are often more restrictive than dynamically-typed languages. In particular, it is desirable to allow strongly-typed languages to have "holes" in the type structure, so that portions of the program that are not fully understood may be written using dynamic typing. There have been several proposals for creating such holes, such as [3, 9, 10]. Typically, one gives the result of such an untyped computation a special type, untyped. Such a value can be passed as an ordinary value, but is not manipulabl..