Shrink fast correctly!

Olivier Savary Bélanger, Andrew W. Appel

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationProceedings of the 19th International Symposium on Principles and Practice of Declarative Programming, PPDP 2017
PublisherAssociation for Computing Machinery
Pages49-60
Number of pages12
ISBN (Electronic)9781450352918
DOIs
StatePublished - Oct 9 2017
Event19th International Symposium on Principles and Practice of Declarative Programming, PPDP 2017 - Namur, Belgium
Duration: Oct 9 2017Oct 11 2017

Publication series

NameACM International Conference Proceeding Series
VolumePart F131196

Other

Other19th International Symposium on Principles and Practice of Declarative Programming, PPDP 2017
CountryBelgium
CityNamur
Period10/9/1710/11/17

All Science Journal Classification (ASJC) codes

  • Software
  • Human-Computer Interaction
  • Computer Vision and Pattern Recognition
  • Computer Networks and Communications

Fingerprint Dive into the research topics of 'Shrink fast correctly!'. Together they form a unique fingerprint.

  • Cite this

    Bélanger, O. S., & Appel, A. W. (2017). Shrink fast correctly! In Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming, PPDP 2017 (pp. 49-60). (ACM International Conference Proceeding Series; Vol. Part F131196). Association for Computing Machinery. https://doi.org/10.1145/3131851.3131859