This paper develops a novel minimal-state operational semantics for higher-order functional languages which uses only the call stack and two source program points as the complete state information: there is no environment, no substitution, no continuation, etc. We prove this form of operational semantics is 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.

翻译：本文提出了一种新颖的最小状态操作语义，适用于高阶函数式语言。该语义仅使用调用栈和两个源程序点作为完整状态信息：不涉及环境、替换、续延等概念。我们证明这种操作语义等价于标准表示形式，并展示该方法如何为潜在新应用开辟道路：通过直接对该操作语义进行有限化处理，定义了一种程序分析。与高阶程序的标准分析相比，这种自然生成的程序分析具有若干新颖且有趣的特性，例如能够推断递归关系且无需值扩展。我们既给出了该分析的形式化定义，也描述了当前的实现。