Skip to main content

Shrink fast correctly!

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

Download
To refer to this page use: http://arks.princeton.edu/ark:/88435/pr1kr7t
Full metadata record
DC FieldValueLanguage
dc.contributor.authorBélanger, Olivier S-
dc.contributor.authorAppel, Andrew W-
dc.date.accessioned2021-10-08T19:44:45Z-
dc.date.available2021-10-08T19:44:45Z-
dc.date.issued2017-10en_US
dc.identifier.citationBé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.3131859en_US
dc.identifier.urihttps://www.cs.princeton.edu/~appel/papers/shrink-fast-correctly.pdf-
dc.identifier.urihttp://arks.princeton.edu/ark:/88435/pr1kr7t-
dc.description.abstractFunction 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.en_US
dc.format.extent49 - 60en_US
dc.language.isoen_USen_US
dc.relation.ispartofInternational Symposium on Principles and Practice of Declarative Programmingen_US
dc.rightsAuthor's manuscripten_US
dc.titleShrink fast correctly!en_US
dc.typeConference Articleen_US
dc.identifier.doi10.1145/3131851.3131859-
pu.type.symplectichttp://www.symplectic.co.uk/publications/atom-terms/1.0/conference-proceedingen_US

Files in This Item:
File Description SizeFormat 
ShrinkFastCorrectly.pdf697.26 kBAdobe PDFView/Download


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