paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Handling Exceptions and Effects with Automatic Resource Analysis

支持异常与效应的自动资源分析
OOPSLA 10(OOPSLA1)2026匹配度 3/10 · 该论文属于纯程序语言与静态分析方向,研究基于类型的自动资源界分析(AARA)对异常与效应处理器的支持,理论性强,但未涉及 LLM/Agent、机器学习系统、浮点程序分析或贝叶斯程序分析,与用户画像的核心交叉方向仅有静态分析这一间接关联。引用 0 inbox
Ethan Chu, Yiyang Guo, Jan Hoffmann
crossref: 2026-09-10

AI 速览

一句话:首个支持异常与效应处理器间非局部控制转移的自动资源界分析,扩展了基于类型的 AARA。

自动推导参数化资源(代价)界的技术已能处理大量语言特性,但异常与效应处理器所需的非局部控制转移一直是难点。本文提出首个支持异常/效应与其处理器之间非局部控制转移的自动资源界分析。该方法扩展了基于类型的自动摊销资源分析(AARA),为带列表和线性 potential 函数的简单函数式语言设计了新的类型系统,并给出一种新颖的语法式类型可靠性定理,相对于基于栈的抽象机器证明所推导界的正确性;其思想可直接推广,并在 Standard ML 与多项式 potential 函数上实现。实验表明,该分析能处理现有方法无法分析的程序,且支持异常与效应处理器的效率开销较低。

问题
自动资源界分析已较成熟,但异常与效应处理器引入的非局部控制转移使现有技术难以给出可靠界。
方法
扩展类型基自动摊销资源分析(AARA),为含列表与线性 potential 的函数式语言建立处理异常与效应的类型系统,并相对栈式抽象机器证明类型可靠性。
评估
在 Standard ML 与多项式 potential 上实现原型,实验显示可分析现有方法无法处理的程序,且支持异常与效应处理器的开销较低。
原文摘要(Abstract)

There exist many techniques for automatically deriving parametric resource (or cost) bounds by analyzing the source code of a program. These techniques work effectively for a large class of programs and language features. However, non-local transfer of control as needed for exception or effect handlers has remained a challenge. This paper presents the first automatic resource bound analysis that supports non-local control transfer between exceptions or effects and their handlers. The analysis is an extension of type-based automatic amortized resource analysis (AARA), which automates the potential method of amortized analysis. It is presented for a simple functional language with lists and linear potential functions. However, the ideas are directly applicable to richer settings and implemented for Standard ML and polynomial potential functions. Apart from the new type system for exceptions and effects, a main contribution is a novel syntactic type-soundness theorem that establishes the correctness of the derived bounds with respect to a stack-based abstract machine. An experimental evaluation shows that the new analysis is capable of analyzing programs that cannot be analyzed by existing methods and that the efficiency overhead of supporting exception and effect handlers is low.

链接与引用

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

BibTeX
@article{paperbot3780,
  title = {Handling Exceptions and Effects with Automatic Resource Analysis},
  author = {Ethan Chu and Yiyang Guo and Jan Hoffmann},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {10},
  number = {OOPSLA1},
  year = {2026},
  doi = {10.1145/3798207}
}