POPL
2004
ACM
14 years 4 months ago
2004
ACM
The ability to summarize procedures is fundamental to building scalable interprocedural analyses. For sequential programs, procedure summarization is well-understood and used rout...
POPL
2004
ACM
14 years 11 months ago
2004
ACM
We present a formalization of the implementation of generics in the .NET Common Language Runtime (CLR), focusing on two novel aspects of the implementation: mixed specialization a...
POPL
2004
ACM
14 years 11 months ago
2004
ACM
We aim to specify program transformations in a declarative style, and then to generate executable program transformers from such specifications. Many transformations require non-t...
POPL
2004
ACM
14 years 11 months ago
2004
ACM
We present a framework for the certification of compilation and of compiled programs. Our approach uses a symbolic transfer functions-based representation of programs, so as to ch...
POPL
2004
ACM
14 years 11 months ago
2004
ACM
Defunctionalization is a program transformation that aims to turn a higher-order functional program into a first-order one, that is, to eliminate the use of functions as first-cla...
POPL
2004
ACM
14 years 11 months ago
2004
ACM
We investigate proof rules for information hiding, using the recent formalism of separation logic. In essence, we use the separating conjunction to partition the internal resource...
POPL
2004
ACM
14 years 11 months ago
2004
ACM
POPL
2004
ACM
14 years 11 months ago
2004
ACM
We define seal, an untyped call-by-value -calculus with primitives for protecting abstract data by sealing, and develop a bisimulation proof method that is sound and complete with...
POPL
2004
ACM
14 years 11 months ago
2004
ACM
stractions from Proofs Ranjit Jhala1 Kenneth L. McMillan2 1 UC San Diego 2 Cadence Berkeley Laboratories We present a technique for using infeasible program paths to automatically ...
POPL
2004
ACM
14 years 11 months ago
2004
ACM
We present a polynomial time randomized algorithm for global value numbering. Our algorithm is complete when conditionals are treated as non-deterministic and all operators are tr...