Constraint-based type inference for polymorphic programs

Precise type information is invaluable for analysis and optimization of computer programs. Constraint-based type inference infers types with subtyping constraints. Such types can capture detailed flow information about a program. Thus constraint-based type inference can be used for extensive type checking and precise flow analysis.; Polymorphism in programming languages makes it difficult for a constraint-based type inference algorithm to be both efficient and accurate. We develop a novel framework for polymorphic constraint-based type inference. A concrete type inference algorithm can be obtained by instantiating the framework with a particular strategy for handling polymorphism. In particular, we define existing algorithms such as Shivers' nCFA and Agesen's Cartesian Product Algorithm (CPA) as instantiations of the framework. We prove the soundness of the framework, which entails the soundness of every algorithm defined as an instantiation of the framework.; Data Polymorphism is a special form of polymorphism associated with programming languages with state, and it is a common and important form of polymorphism in object-oriented programming. Agesen's Cartesian Product Algorithm (CPA) can analyze programs with parametric polymorphism in a reasonably precise and efficient manner, but CPA is imprecise when analyzing programs with data polymorphism. We have developed a novel algorithm, Data Polymorphic CPA (DCPA), a constraint-based type inference algorithm that extends CPA with the ability to accurately and efficiently analyze data-polymorphic programs.; We also study the construction of practical constraint-based type inference systems for realistic programming languages. We have constructed a type inference system for the full Java language. The system includes implementations of algorithms 0CFA, CPA and DCPA, and it has incorporated a number of novel implementation techniques. The system is used to statically verify the correctness of Java downcasts. Benchmark results on realistic Java applications are given which show that the DCPA algorithm has good precision and efficiency: it is significantly more accurate than CPA and its efficiency is comparable to CPA.