In programming languages, existential quantification is useful for describing
relationships among members of a structured type.  For example, we may have a
list in which there exists some mutual exclusion lock l in each list element
such that l  protects the data stored in that element. With this information, a
static analysis can reason about the relationship between locks and locations
in the list even when the precise identity of the lock and/or location is
unknown. To facilitate the construction of such static analyses, this paper
presents a context-sensitive label flow analysis algorithm with support for
existential quantification. Label flow analysis is a core part of many static
analysis systems. Following Rehof et al, we use context-free language (CFL)
reachability to develop an efficient O(n^3) label flow inference algorithm. We
prove the algorithm sound by reducing its derivations to those in a system
based on polymorphically-constrained types, in the style of Mossin.  We have
implemented a variant our analysis as part of a data race detection tool for C
programs.