To refer to this page use:
|Abstract:||Function inlining, case-folding, projection-folding, and dead-variable elimination are important code transformations in virtually every functional-language compiler. When one of these reductions strictly reduces the size of the program (e.g., when the inlined function has only one applied occurrence), we call it a shrink reduction. Appel and Jim  introduced an algorithm to perform all shrink reductions (producing a shrink normal form) in quasilinear time. They proved confluence but not correctness. We have implemented this algorithm as part of an end-to-end verified compiler for Gallina, the specification language of the Coq theorem prover. We have given the first proofs of these properties: correctness with respect to contextual equivalence, reduction (in one pass) of all administrative redexes with one applied occurrence introduced by CPS conversion, and termination. The correctness and termination proofs are machine-checked in Coq. Because we use a pure functional language without imperative array update, our implementation is O(N log N) rather than O(N). Still, it's quite fast: we give performance results on some nontrivial benchmarks.|
|Citation:||Bélanger, Olivier Savary, and Andrew W. Appel. "Shrink fast correctly!" In Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming (2017): pp. 49-60. doi: 10.1145/3131851.3131859|
|Pages:||49 - 60|
|Type of Material:||Conference Article|
|Journal/Proceeding Title:||International Symposium on Principles and Practice of Declarative Programming|
Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.