Constraint abstractions

Abstract. Many type based program analyses with subtyping, such as flow analysis, are based on inequality constraints over a lattice. When inequality constraints are combined with polymorphism it is often hard to scale the analysis up to large programs. A major source of inefficiency in conventional implementations stems from computing substitution in-stances of constraints. In this paper we extend the constraint language with constraint abstractions so that instantiation can be expressed di-rectly in the constraint language and we give a cubic-time algorithm for constraint solving. As an application, we illustrate how a flow analysis with flow subtyping, flow polymorphism and flow-polymorphic recursion can be implemented in O(n3) time where n is the size of the explicitly typed program.