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

翻译：从程序中消除高阶函数的去函数化转换在许多编译器中扮演着关键角色。然而，针对依赖类型语言的去函数化尚未得到正式研究。我们首次提出了针对依赖类型语言的形式化去函数化转换，并确立了关键元理论性质，如可靠性和类型保持性。该转换适用于集成到依赖类型语言的类型保持编译器中。