CMSC 32001: Topics in Programming Languages

The focus of this seminar will be Higher-Order Control-Flow Analysis (CFA) with a dash of automated meta-theory in the second half of the quarter. We will be reading and discussing a number of the significant papers in the area; in the later part of the term, we will investigate proving the correctness of Matt Might’s reference implementation of k-CFA.

For a first-order language (i.e., C or Fortran), the syntax of the language defines a control-flow graph (CFG) for the body of a function. Furthermore, we can easily extend this to a call-graph (or inter-procedural CFG) for most programs. Given such a graph, we can perform various data-flow analyses to guide optimization or to check program properties.

For higher-order languages, however, the target of control transfers depends on evaluating an expression that produces a function (in functional languages) or object (in object-oriented languages). Thus, before we can perform data-flow analysis, we must first perform an analysis to determine the CFG (or an approximation) of it. But since functions/objects are just another kind of data, we need to simultaneously perform a data-flow analysis. A further problem is that functions are not just code, but also have an environment that defines the free variables of the function.

TBA