Abstracting Denotational Interpreters
arxiv(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要