We explore denotational interpreters: denotational semantics that produce coinductive traces of a corresponding small-step operational semantics. By parameterising our denotational interpreter over the semantic domain and then varying it, we recover dynamic semantics with different evaluation strategies as well as summary-based static analyses such as type analysis, all from the same generic interpreter. Among our contributions is the first denotational semantics for call-by-need that is provably adequate in a strong, compositional sense. The generated traces lend themselves well to describe operational properties such as how often a variable is evaluated, and hence enable static analyses abstracting these operational properties. Since static analysis and dynamic semantics share the same generic interpreter definition, soundness proofs via abstract interpretation decompose into showing small abstraction laws about the abstract domain, thus obviating complicated ad-hoc preservation-style proof frameworks.

翻译：本文探讨指称解释器：一种能够生成对应小步操作语义的共归纳迹的指称语义方法。通过将指称解释器参数化于语义域并对其进行变换，我们可以从同一个通用解释器中推导出具有不同求值策略的动态语义，以及基于摘要的静态分析（如类型分析）。我们的主要贡献之一是首次提出了按需调用（call-by-need）的指称语义，该语义在强组合意义上被证明是充分的。生成的迹能很好地描述操作属性，例如变量被求值的频率，从而支持对这些操作属性进行抽象的静态分析。由于静态分析与动态语义共享相同的通用解释器定义，基于抽象解释的正确性证明可分解为展示抽象域上的小型抽象定律，从而避免了复杂的临时性保持式证明框架。