If you agree with this copyright notice, you can get the paper:
We give a new correctness proof starting directly from a semantics. Contrary to previous proofs, it takes into account all the features of functional languages, including imperative features and polymorphism. The analysis has been designed so that it can be implemented under the small complexity bound of O(n log2 n) where n is the size of the analyzed program. We have included it in the Caml Special Light compiler (an implementation of ML), and applied it to very large programs. We plan to apply these techniques to the Java programming language.
Escape analysis has been applied to stack allocation. We improve the optimization technique by determining minimal lifetime for stack allocated data, and using inlining. We manage to stack allocate 25% of data in the theorem prover Coq. We analyzed the effect of this optimization, and noticed that its main effect is to improve data locality, which is important for efficiency.
@INPROCEEDINGS{BlanchetPOPL98, AUTHOR = {Bruno Blanchet}, TITLE = {Escape {A}nalysis: Correctness {P}roof, {I}mplementation and {E}xperimental {R}esults}, BOOKTITLE = {25th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL'98)}, YEAR = 1998, PUBLISHER = {ACM Press}, ADDRESS = {San Diego, California}, MONTH = JAN, PAGES = {25--37} }