paperbot · PL 论文追踪

全部论文 待读 收藏

P1 Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages

高阶语言中的环境共享分析与调用者提供环境
ICFP 9(ICFP)2025匹配度 5/10 · 该论文属于经典的程序分析与抽象解释,涉及高阶控制流分析和形式化验证,方法与用户对静态分析及理论形式化的兴趣相关;但它不涉及 LLM/Agent、浮点程序分析或贝叶斯程序分析,与用户核心的 PL×AI 交叉方向距离较远。引用 2 inbox
J. A. Carr, Benjamin Quiring, John Reppy, Olin Shivers, Skye Soss, Byron Zhong
crossref: 2026-09-10

AI 速览

一句话:提出基于抽象解释的高阶环境共享分析并形式化,支持调用者提供环境以减少环境分配。

高阶语言中,函数表示包含代码与捕获自由变量的环境结构。本文研究“调用者提供环境”:不再由闭包打包全部环境,而允许调用者在调用点提供函数环境的一部分。由于高阶语言难以静态确定调用点及可用环境片段,作者提出一种新的基于抽象解释的分析,发现函数定义与调用者之间总是共享的环境片段,从而可由调用者传入。该分析在Rocq证明助手中形式化。对一组程序的评估表明,它可扩展,且比常见语法方法和轻量闭包转换提供更精确信息,许多程序上达到理论上界。论文还讨论如何避免额外运行时开销的变换决策,并通过插桩解释器评估,证明能有效减少环境动态分配。

问题
高阶语言中函数闭包需打包自由变量环境,但调用点难以静态确定,导致难以让调用者提供被调函数的部分环境并避免额外开销。
方法
提出基于抽象解释的环境共享分析,静态发现函数定义与调用者总是共享的环境片段,并在Rocq中形式化;据此设计调用者提供环境的程序变换决策。
评估
在一组程序上评估分析的可扩展性与精度,与语法方法和轻量闭包转换比较,许多程序达到理论上界;并用插桩解释器衡量变换效果,显示可减少环境动态分配。
原文摘要(Abstract)

The representation of functions in higher-order languages includes both the function’s code and an environment structure that captures the bindings of the function’s free variables. This paper explores caller-provided environments, where instead of packaging the entirety of a function’s environment in its closure, a function can be provided with a portion of its environment by its caller. In higher-order languages, it is difficult to determine where functions are called, let alone what pieces of the function’s environment are available to be provided by the caller, thus we need a higher-order control-flow analysis to enable caller-provided environments. In this paper, we present a new abstract-interpretation-based analysis that discovers which pieces of a function’s environment are always shared between its definition and its callers. In such cases, the caller can provide the environment to the callee. Our analysis has been formalized in the Rocq proof assistant. We evaluate our analysis on a collection of programs demonstrating that it is both scalable and provides significantly better information over the common syntactic approach and better information than lightweight closure conversion . In fact, it yields the theoretical upper-bound for many programs. For caller-provided environments, deciding how to transform the program based on these revealed facts is also non-trivial and has the potential to incur extra runtime cost over standard strategies. We discuss how to make these decisions in a way that avoids the extra costs and how to transform a program accordingly. We also propose other uses of the analysis results beyond enabling caller-provided environments. We evaluate our transformation using an instrumented interpreter, showing that our approach is effective in reducing dynamic allocations for environments.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot3031,
  title = {Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages},
  author = {J. A. Carr and Benjamin Quiring and John Reppy and Olin Shivers and Skye Soss and Byron Zhong},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {9},
  number = {ICFP},
  year = {2025},
  doi = {10.1145/3747516}
}