Existential Label Flow Inference via CFL Reachability
| dc.contributor.author | Pratikakis, Polyvios | |
| dc.contributor.author | Hicks, Michael | |
| dc.contributor.author | Foster, Jeffrey S. | |
| dc.date.accessioned | 2005-11-10T20:04:41Z | |
| dc.date.available | 2005-11-10T20:04:41Z | |
| dc.date.issued | 2005-11-10T20:04:41Z | |
| dc.description.abstract | 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^3) 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. | en |
| dc.format.extent | 442788 bytes | |
| dc.format.mimetype | application/pdf | |
| dc.identifier.uri | http://hdl.handle.net/1903/3018 | |
| dc.language.iso | en_US | en |
| dc.relation.ispartofseries | UM Computer Science Department | en |
| dc.relation.ispartofseries | CS-TR-4700 | en |
| dc.title | Existential Label Flow Inference via CFL Reachability | en |
| dc.type | Technical Report | en |