A Pure Demand Operational Semantics with Applications to Program Analysis
Proceedings of the ACM on Programming Languages(2023)
摘要
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.
更多查看译文
关键词
Demand-Driven Operational Semantics
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要