We show how control-flow-based program transformations in functional languages can be proven correct. The method relies upon "defunctionalization," a mapping from a higher-order language to a first-order language. We give methods for proving defunctionalization correct. Using this proof and common semantic techniques, we then show how two program transformations---flow-based inlining and lightweight defunctionalization---can be proven correct.
Joint with Nevin Heintze and Jon G. Riecke, Bell Laboratories
A number of security systems for programming languages have recently
appeared, including systems for enforcing some form of
access control. The Java JDK 1.2 security architecture is
one such system that is widely studied and used. While the
architecture has many appealing features, access control checks are
all implemented via dynamic method calls. This is a highly
non-declarative form of specification which is hard to read, and
which leads to additional run-time overhead. In this paper, we
present a novel security type system that enforces the same
security guarantees as Java Stack Inspection, but via a static type
system with no additional run-time checks. The system allows
security properties of programs to be clearly expressed within the
types themselves. We also define and prove correct an inference
algorithm for security types, meaning that the system has the
potential to be layered on top of the existing Java architecture,
without requiring new syntax.
We present an algorithm for constructing the minimal static
single assignment form (SSA) of arbitrary flowgraphs in time
linear in sizes of the input program and the SSA form output,
under the assumption that there is at least one assignment in each
basic block. As far as we know, this is the first optimal
algorithm for SSA construction. The crucical data structure that
we use is the compressed DJ-graph, a variant of the DJ-graph with
``short-cuts'', which allows online queries of IDF(N_\alpha) the
iterated dominance frontier of a set N_\alpha, to complete in
O(|N_\alpha| + \sum_{x \in IDF(N_\alpha)} indeg(x)) time.
Compressed DJ-graph is not restricted to SSA computation and can
be also used to speed up various compiler optimization problems
which involve the computation of (iterated) dominance frontier,
such as sparse evaluation graph construction.
The CIL ML compiler uses intersection and union types, with flow information incorporated into the types, to facilitate using specialized data representations. We will present the latest empirical results from experimenting with using Steckler's "selective closure conversion" representation on a number of standard ML benchmarks.