A Type- and Control-Flow Analysis for System F

Abstract. We present a monovariant flow analysis for System F (with recursion). The flow analysis yields both control-flow information, ap-proximating the λ- and Λ-expressions that may be bound to variables, and type-flow information, approximating the type expressions that may instantiate type variables. Moreover, the two flows are mutually bene-ficial: the control flow determines which Λ-expressions may be applied to which type expressions (and, hence, which type expressions may in-stantiate which type variables), while the type flow filters the λ- and Λ-expressions that may be bound to variables (by rejecting expressions with static types that are incompatible with the static type of the vari-able under the type flow). As is typical for a monovariant control-flow analysis, control-flow information is expressed as an abstract environ-ment mapping variables to sets of (syntactic) λ- and Λ-expressions that occur in the program under analysis. Similarly, type-flow information is expressed as an abstract environment mapping type variables to sets o