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.

翻译：本文为高阶函数式语言发展了一种新颖的最小状态操作语义，仅使用调用栈和源程序点或词法层级作为完整的状态信息：无需环境、替换、续延等。我们证明了这种操作语义形式与标准表示等价。随后展示了该方法如何为潜在的新应用开辟道路：我们将程序分析定义为该操作语义的直接有限化。相较于高阶程序的标准程序分析，这种自然产生的程序分析具有若干新颖有趣的特性：例如，它能够推断递归关系且无需值扩展。我们既给出了该分析的形式化定义，也描述了当前的实现方案。