The Complexity of Flow Analysis in Higher-Order Languages: Abstract, Dissertation, Slides.
PhD Thesis Defense
Computer Science Department
Brandeis University
Date: Wednesday, July 22, 2009
Time: 2-4pm
Place: Volen 101
The Complexity of Flow Analysis in Higher-Order Languages
David Van Horn
Abstract:
This dissertation proves lower bounds on the inherent difficulty of deciding flow analysis problems in higher-order programming languages. We give exact characterizations of the computational complexity of 0CFA, the kCFA hierarchy, and related analyses. [...]
CSL’09 will include a satellite workshop on linearity:
Linearity has been the key feature in several lines of research in both theoretical and practical approaches to computer science. In the theoretical side all the work stemming from linear logic dealing with proof technology, complexity classes and more recently quantum computation. In the practical side work on [...]
From Robert J. Simmons’ list of a papers is this “wordle” for “Linear Logical Approximations”, Simmons and Pfenning, PEPM 2008. If you look closely, you can see I’ve made a mark (or two).
Flow analysis, linearity, and PTIME was accepted at this year’s Static Analysis Symposium (SAS). An early preprint was announced here, but the presentation has benefitted significantly from the anonymous reviewers’ comments. Also, the abstract was rewritten to be somewhat comprehensible (thanks to Dave Herman for encouraging the rewrite).
Flow analysis is a ubiquitous [...]
My other par is a lambda.
Saturday, February 2, 2008
Harry has just returned from CMU after giving a talk on our recent work on the complexity of CFA. The slides are available here. As usual, they’re very funny and insightful. It summarizes not only our 2007 ICFP paper, but our recent unpublished result showing that for any fixed k > 0, [...]
Saturday, February 2, 2008
A new preprint is available: Linearity, flow analysis, and PTIME. Harry and I show that not only is 0CFA exact for linear terms, but it remains exact for approximations to and restrictions of 0CFA (this is true for all of the analyses I could find in the literature). Because of this exactness, normalization [...]
Tuesday, November 6, 2007
Mairson has an encoding of the Booleans in the linear lambda calculus, which improves upon the usual Church encoding which is linear affine. Typically Mairson’s encoding is presented in linear ML to take advantage of pattern matching and tuples, but it is easy enough to present the embedding in linear Scheme using only unary [...]
Wednesday, October 17, 2007
Linearity is the key to subverting the approximation of any monovariant analysis, like simple typing or 0CFA, and renders the analysis synonymous with normalization. However, something weird happens in the case of (k > 0)CFA: linear expansion does not preserve the precision of the analysis. For example, take the program:
(λf.f f (λy.y)) (λx.x)
This [...]