Skip to main content

Shrink fast correctly!

Author(s): Bélanger, Olivier S; Appel, Andrew W

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 [1] 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.
Publication Date: Oct-2017
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
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
Version: Author's manuscript

Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.