Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Pure Demand Operational Semantics with Applications to Program Analysis

Scott Smith, Robert Zhang

Abstract

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.

A Pure Demand Operational Semantics with Applications to Program Analysis

Abstract

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.
Paper Structure (43 sections, 16 theorems, 6 equations, 22 figures, 1 table)

This paper contains 43 sections, 16 theorems, 6 equations, 22 figures, 1 table.

Table of Contents

  1. Introduction
  2. A Pure Demand Program Analysis
  3. Summary of Contributions
  4. Outline
  5. A Pure Demand Operational Semantics
  6. The Core Language
  7. The Rules
  8. On-Demand Variable Lookup
  9. An Example
  10. From Access Links to Displays
  11. An Extended Language
  12. Efficiency
  13. Soundness
  14. Environment/Closure-Based System
  15. Chaining Variable Lookups Directly
  16. ...and 28 more sections

Key Result

lemma 1

Any variable lookup subtree in a proof of $\Sigma \vdash \expr \Rightarrow \reval$ must be of the form of Figure fig_variable_lookup_canonical.

Figures (22)

  • Figure 1: Language and interpreter grammar
  • Figure 2: Pure demand operational semantics rules
  • Figure 3: An example derivation using the rules of figure \ref{['fig_steps']}
  • Figure 4: Extended language grammar
  • Figure 5: Operational semantics with displays
  • ...and 17 more figures

Theorems & Definitions (29)

  • definition 1
  • definition 2
  • definition 3: Result Evaluation
  • definition 4
  • definition 5
  • definition 6
  • lemma 1
  • lemma 2
  • definition 7
  • lemma 3
  • ...and 19 more