一句话：提出仅用调用栈和程序点/词法层作为状态的纯需求操作语义，并将其有限化直接导出高阶程序分析。
本文面向高阶函数式语言，提出一种极小状态的操作语义：程序状态仅由调用栈以及源程序点或词法层级组成，不显式维护环境、替换或续延等结构。作者证明该语义与标准操作语义等价。进一步，通过将该操作语义直接有限化，得到一种自然的程序分析；该分析能够推断递归/递推关系，并且不需要传统的值加宽。文章给出分析的形式定义，并介绍当前实现。该工作为程序分析提供了从语义定义直接构造分析的新途径。
This paper develops a novel minimal-state operational semantics for higher-order functional languages that uses only the call stack and a source program point or a lexical level as the complete state information: there is no environment, no substitution, no continuation, etc. We prove this form of operational semantics equivalent to standard presentations. We then show how this approach can open the door to potential new applications: we define a program analysis as a direct finitization of this operational semantics. The program analysis that naturally emerges has a number of novel and interesting properties compared to standard program analyses for higher-order programs: for example, it can infer recurrences and does not need value widening. We both give a formal definition of the analysis and describe our current implementation.
@article{paperbot2546,
title = {A Pure Demand Operational Semantics with Applications to Program Analysis},
author = {Scott Smith and Robert Zhang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA1},
year = {2024},
doi = {10.1145/3649852}
}