A verified framework for higher-order uncurrying optimizations

Abstract : Function uncurrying is an important optimization for the efficient execution of functional programming languages. This optimization replaces curried functions by uncur-ried, multiple-argument functions, while preserving the ability to evaluate partial applications. First-order uncurrying (where curried functions are optimized only in the static scopes of their definitions) is well understood and implemented by many compilers, but its extension to higher-order functions (where uncurrying can also be performed on parameters and results of higher-order functions) is challenging. This article develops a generic framework that expresses higher-order uncurrying optimizations as type-directed insertion of coercions, and prove its correctness. The proof uses step-indexed logical relations and was entirely mechanized using the Coq proof assistant.
Document type :
Journal articles
Liste complète des métadonnées

Cited literature [37 references]  Display  Hide  Download

https://hal.inria.fr/hal-01499915
Contributor : Xavier Leroy <>
Submitted on : Saturday, April 1, 2017 - 3:36:51 PM
Last modification on : Thursday, February 7, 2019 - 4:22:16 PM
Document(s) archivé(s) le : Sunday, July 2, 2017 - 12:41:27 PM

File

higher-order-uncurrying.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Zaynah Dargaye, Xavier Leroy. A verified framework for higher-order uncurrying optimizations. Higher-Order and Symbolic Computation, Springer Verlag, 2009, 22 (3), 〈10.1007/s10990-010-9050-z〉. 〈hal-01499915〉

Share

Metrics

Record views

261

Files downloads

48