[Pl-seminar] Semantics Seminar Schedule

[Mitchell Wand]

NU Programming Languages Seminar
Wednesday, 5/23/07  (** that's NEXT Wed, not tomorrow 5/16 **)
11:45am-1:30pm
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Relating Complexity and Precision in Control Flow Analysis
David Van Horn 

We analyze the computational complexity of kCFA, a hierarchy of control
flow analyses that determine which functions may be applied at a given
call-site. This hierarchy specifies related decision problems, quite
apart from any algorithms that may implement their solutions. We
identify a simple decision problem answered by this analysis and prove
that in the 0CFA case, the problem is complete for polynomial time. The
proof is based on a nonstandard, symmetric implementation of Boolean
logic within multiplicative linear logic (MLL). We also identify a
simpler version of 0CFA related to eta-expansion, and prove that it is
complete for LOGSPACE, using arguments based on computing paths and
permutations.

For any fixed k>0, it is known that kCFA (and the analogous decision
problem) can be computed in time exponential in the program size. For
k=1, we show that the decision problem is NP-hard, and sketch why this
remains true for larger fixed values of k. The proof technique depends
on using the approximation of CFA as an essentially nondeterministic
computing mechanism, as distinct from the exactness of normalization.
When k=n, so that the ``depth'' of the control flow analysis grows
linearly in the program length, we show that the decision problem is
complete for EXPTIME.

In addition, we sketch how the analysis presented here may be extended
naturally to languages with control operators. All of the insights
presented give clear examples of how straightforward observations about
linearity, and linear logic, may in turn be used to give a greater
understanding of functional programming and program analysis.

(joint work with Harry Mairson)

Upcoming Events:

# 5/30 Torben Amtoft
# Don't you want to speak at pl-seminar?

--Mitch