paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Defunctionalization with Dependent Types

带依赖类型的去函数化
PLDI 7(PLDI)2023匹配度 1/10 · 该论文研究依赖类型语言的去函数化翻译及其元理论性质，属于纯 PL/类型系统与编译方向，未涉及用户核心关注的 LLM/Agent、机器学习系统静态分析、浮点程序分析或贝叶斯程序分析。引用 4 inbox
Yulong Huang, Jeremy Yallop
类型系统编译与代码生成
crossref: 2026-09-10

AI 速览

一句话：首次为依赖类型语言形式化定义去函数化翻译，并证明其可靠性与类型保持。

论文关注高阶函数在依赖类型语言中的编译变换问题：现有去函数化虽广泛用于编译器，却未被形式化研究。作者为依赖类型语言设计并形式化规定了首个去函数化翻译，将高阶函数消除为具体的数据类型与函数应用，并建立关键元理论性质，包括翻译的可靠性与类型保持。该翻译适合纳入依赖类型语言的类型保持编译器，为后续实现与验证提供基础。

问题
依赖类型语言中，用于消除高阶函数的去函数化翻译此前缺乏形式化研究。
方法
提出首个针对依赖类型语言的形式化去函数化翻译，并建立可靠性与类型保持等元理论性质。
评估
评估方式为形式化定义该翻译并证明其可靠性与类型保持等元理论性质。
原文摘要（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

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@article{paperbot1965,
  title = {Defunctionalization with Dependent Types},
  author = {Yulong Huang and Jeremy Yallop},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {7},
  number = {PLDI},
  year = {2023},
  doi = {10.1145/3591241}
}