Defunctionalization with Dependent Types
Programming Languages
2023-04-11 v1
Abstract
The defunctionalization translation that eliminates higher-order functions from programs forms a key part of many compilers. However, defunctionalization for dependently-typed languages has not been formally studied. We present the first formally-specified defunctionalization translation for a dependently-typed language and establish key metatheoretical properties such as soundness and type preservation. The translation is suitable for incorporation into type-preserving compilers for dependently-typed languages
Cite
@article{arxiv.2304.04574,
title = {Defunctionalization with Dependent Types},
author = {Yulong Huang and Jeremy Yallop},
journal= {arXiv preprint arXiv:2304.04574},
year = {2023}
}