Type-based flow analysis:: From polymorphic subtyping to CFL-reachability.

We present a novel approach to scalable implementation of type-based flow analysis with polymorphic subtyping. Using a new presentation of polymorphic subtyping with instantiation constraints, we are able to apply context-free language (CFL) reachability techniques to type-based how analysis. We develop a CFL-based algorithm for computing flow information in time O(n(3)), where n is the size of the typed program. The algorithm substantially improves upon the best previously known algorithm for how analysis based on polymorphic subtyping with complexity O(n(8)). Our technique also yields the first, demand-driven algorithm for polymorphic subtype-based flow-computation. It works directly on higher-order programs with structured data of finite type (unbounded data structures are incorporated via finite approximations), supports context-sensitive, global how summarization and includes polymorphic recursion.