paperbot · PL 论文追踪

全部论文 待读 收藏

P2 A calculus of expandable stores

一种可扩展存储的演算
LICS Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science2020匹配度 1/10 · 该论文属于纯程序语言理论中的形式语义研究,讨论 call-by-need 抽象机中全局环境(可扩展存储)的演算与 CPS 翻译,与用户关注的方向(静态分析及其与 ML/LLM/Agent 的交叉、浮点程序分析、贝叶斯程序分析)没有实质交集。虽然同属 PL 领域且兼具形式化特点,但既非问题驱动的分析工具研究,也不涉及任何 AI/LLM 或工程落地场景。引用 1 inbox
Hugo Herbelin, Étienne Miquey
crossref: 2026-09-12

AI 速览

一句话:提出可扩展存储的演算,为带全局环境的 call-by-need 抽象机及其 CPS 翻译提供形式化基础。

call-by-need 是 λ-演算的一种惰性求值策略:只在需要时求值参数,并在所有使用处共享计算结果。实现该策略的抽象机通常需要某种全局环境。抽象机有助于理解执行过程中的控制流,尤其便于定义 continuation-passing style(CPS)翻译;然而,带有全局环境的抽象机在形式上更为微妙。本文提出一种可扩展存储(expandable stores)的演算,旨在为这类 call-by-need 抽象机提供合适的演算刻画,从而更清晰地分析其控制流与 CPS 翻译。

问题
带全局环境的 call-by-need 抽象机在控制流理解与 CPS 翻译定义上比普通抽象机更微妙,缺乏合适的演算刻画。
方法
提出可扩展存储的演算,以存储扩展为基本机制来建模 call-by-need 的惰性求值与共享,并分析此类抽象机的行为。
评估
摘要未给出实验或机器化验证等评估细节,具体评估方式未在摘要中说明。
原文摘要(Abstract)

The call-by-need evaluation strategy for the λ-calculus is an evaluation strategy that lazily evaluates arguments only if needed, and if so, shares computations across all places where it is needed. To implement this evaluation strategy, abstract machines require some form of global environment. While abstract machines usually lead to a better understanding of the flow of control during the execution, facilitating in particular the definition of continuation-passing style translations, the case of machines with global environments turns out to be much more subtle.

链接与引用

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

BibTeX
@inproceedings{paperbot5488,
  title = {A calculus of expandable stores},
  author = {Hugo Herbelin and Étienne Miquey},
  booktitle = {LICS},
  year = {2020},
  doi = {10.1145/3373718.3394792}
}