### 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 language | English (US) |
---|---|

Title of host publication | Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming, PPDP 2017 |

Publisher | Association for Computing Machinery |

Pages | 49-60 |

Number of pages | 12 |

ISBN (Electronic) | 9781450352918 |

DOIs | |

State | Published - Oct 9 2017 |

Event | 19th International Symposium on Principles and Practice of Declarative Programming, PPDP 2017 - Namur, Belgium Duration: Oct 9 2017 → Oct 11 2017 |

### Publication series

Name | ACM International Conference Proceeding Series |
---|---|

Volume | Part F131196 |

### Other

Other | 19th International Symposium on Principles and Practice of Declarative Programming, PPDP 2017 |
---|---|

Country | Belgium |

City | Namur |

Period | 10/9/17 → 10/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

*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