Typed compilation of inclusive subtyping

I present a type-preserving translation that eliminates subtyping and bound ed quantification without introducing any run-time costs. This translation is based on Mitchell and Pierce's encoding of bounded quantification using intersection types. I show that, previous negative observations notwithstan ding, the encoding is adequate given a sufficiently rich target type theory . The necessary target type theory is made easily typecheckable by includin g a collection of explicit coercion combinators, which are already desired for eliminating subtyping. However, no form of coercion abstraction is nece ssary (even to support bounded quantification), leading to a simple target language.