Label flow analysis is a fundamental static analysis problem with a wide variety of applications. Previous work by Mossin developed a polynomial time subtyping-based label flow inference that supports Hindley-Milner style polymorphism with polymorphic recursion. Rehof et al have developed an efficient O(n³) inference algorithm for Mossin's system based on context-free language (CFL) reachability. In this paper, we extend these results to a system that also supports existential polymorphism, which is important for precisely describing correlations among members of a structured type, even when values of that type are part of dynamic data structures. We first develop a provably sound checking system based on polymorphically-constrained types. As usual, we restrict universal quantification to the top level of a type, but existential quantification is first class, with subtyping allowed between existentials with the same binding structure. We then develop a CFL-based inference system. Programmers specify which positions in a type are existentially quantified, and the algorithm infers the constraints bound in the type, or rejects a program if the annotations are inconsistent.

[ .pdf ]

@techreport{pratikakis05existstr,
  author = {Polyvios Pratikakis and Michael Hicks and Jeffrey S. Foster},
  title = {Existential Label Flow Inference via {CFL} Reachability (Extended Version)},
  institution = {Department of Computer Science, University of Maryland},
  number = {CS-TR-4700},
  year = 2005,
  month = jul
}

This file was generated by bibtex2html 1.99.