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 provably adequate denotational semantics for call-by-need. The generated traces lend themselves well to describe operational properties such as evaluation cardinality, and hence to 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）提供了可证明充分的指称语义。生成的迹很适合描述求值基数等操作性质，进而可对这类操作性质进行抽象化静态分析。由于静态分析与动态语义共享相同的通用解释器定义，通过抽象解释进行的正确性证明可分解为证明关于抽象域的小规模抽象律，从而无需使用复杂的特设保持风格证明框架。