A Pure Demand Operational Semantics with Applications to Program Analysis

This paper develops a novel minimal-state operational semantics forhigher-order functional languages that uses only the call stack and a sourceprogram point or a lexical level as the complete state information: there is noenvironment, no substitution, no continuation, etc. We prove this form ofoperational semantics equivalent to standard presentations. We then show how this approach can open the door to potential newapplications: we define a program analysis as a direct finitization of thisoperational semantics. The program analysis that naturally emerges has a numberof novel and interesting properties compared to standard program analyses forhigher-order programs: for example, it can infer recurrences and does not needvalue widening. We both give a formal definition of the analysis and describeour current implementation.