Type- and Control-Flow Analysis

  • An Efficient Type- and Control-Flow Analysis for System F
    ifl14.pdf (with Connor Adsit; Accepted to IFL'14 (post-proceedings))
    ifl14.orig.pdf (with Connor Adsit; Presented at IFL'14; ifl14_talk.orig.pdf)

    At IFL'12, we presented a novel monovariant flow analysis for System F (with recursion) that yields both type-flow and control-flow information. The type-flow information approximates the type expressions that may instantiate type variables and the control-flow information approximates the λ- and Λ-expressions that may be bound to variables. Furthermore, the two flows are mutually beneficial: control flow determines which Λ-expressions may be applied to which type expressions (and, hence, which type expressions may instantiate which type variables), while 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 variable under the type flow).

    Using a specification-based formulation of the type- and control-flow analysis, we proved the analysis to be sound, decidable, and computable. Unfortunately, naively implementing the analysis using a standard least fixed-point iteration yields an O(n13) algorithm.

    In this work, we give an alternative flow-graph-based formulation of the type- and control-flow analysis. We prove that the flow-graph-based formulation induces solutions satisfying the specification-based formulation and, hence, that the flow-graph-based formulation of the analysis is sound. We give a direct algorithm implementing the flow-graph-based formulation of the analysis and demonstrate that it is O(n4). By distinguishing the size l of expressions in the program from the size m of types in the program and performing an amortized complexity analysis, we further demonstrate that the algorithm is O(l3 + m4).

  • An Efficient Type- and Control-Flow Analysis for System F
    gccisphd_talk.pdf (Presented at Rochester Institute of Technology — GCCIS PhD Colloquium Series (201409260))

    We present a monovariant flow analysis for System F (with recursion). The flow analysis yields both control-flow information, approximating 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 beneficial: the control flow determines which Λ-expressions may be applied to which type expressions (and,hence, which type expressions may instantiate 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 variable under the type flow). We first give a specification-based formulation of the type- and control-flow analysis. Incompatibility of static types (with free type variables) under a type flow is decided by interpreting the type flow as a regular-tree grammar and performing intersection and emptiness operations. Unfortunately, naively implementing the analysis using a standard least fixed-point iteration technique yields an O(n13) algorithm, due to the cost of the regular-tree grammar operations in an inner loop. We next give an alternative flow-graph-based formulation of the type- and control-flow analysis. We give a direct algorithm implementing the flow-graph-based formulation of the analysis and demonstrate that it is O(n4). By distinguishing the size l of terms in the program from the size m of types in the program and performing an amortized complexity analysis, we further demonstrate that the algorithm is O(l3 + m4).

  • A Type- and Control-Flow Analysis for System F
    pldg_talk.pdf (Presented at Cornell University — Programming Language Discussion Group (20130220))

  • A Type- and Control-Flow Analysis for System F
    ifl12.pdf techrpt.pdf (Accepted to IFL'12 (post-proceedings))
    ifl12.orig.pdf techrpt.orig.pdf (Presented at IFL'12; ifl12_talk.orig.pdf; video)

    We present a monovariant flow analysis for System F (with recursion). The flow analysis yields both control-flow information, approximating 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 beneficial: the control flow determines which Λ-expressions may be applied to which type expressions (and, hence, which type expressions may instantiate 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 variable under the type flow). As is typical for a monovariant control-flow analysis, control-flow information is expressed as an abstract environment 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 of (syntactic) types that occur in the program under analysis. Compatibility of static types (with free type variables) under a type flow is decided by interpreting the abstract environment as productions for a regular-tree grammar and querying if the languages generated by taking the types in question as starting terms have a non-empty intersection.


The documents contained in these directories are included by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.