Higher-Order Demand-Driven Symbolic Evaluation
summary
Presents DDSE, a demand-driven symbolic evaluator for higher-order functional code that runs backward from a program point; defines a novel DDI interpreter without substitution, environments, or closures and proves the backward lookup is isomorphic to forward semantics and that the symbolic variant is sound and complete. Ships an OCaml proof-of-concept test generator that finds concrete inputs reaching target lines, uses a coroutine non-determinism monad to prune infinite paths, handles recursion and arbitrary datatypes, and passes benchmarks from a prior forward symbolic executor.
AI-written summary · about
chapters (12)
- 0:00Intro
- 0:14Forward vs Demand in Varying Domains
- 2:20Outline
- 2:32Language Features in this Work
- 3:34The DDI Lookup Function
- 5:00Tracing Function Application
- 6:14Non-Local Variables
- 9:09Peek at Full Rules for Functional Core
- 9:22From Demand Interpreter to Demand Symbolic Evaluation
- 11:17Formal Development
- 12:18DDSE Implementation
- 13:04Comparison with Select Related Work
related talks
29mPartially Evaluating Symbolic Interpreters for All
16mCompiling Symbolic Execution with Staging and Algebraic Effects
24mSymbolic Execution with Separating Decision Diagrams
01h 04mEDSL Infinity Wars: Mainstreaming Symbolic Computation
22mCategorical Semantics of Probabilistic Symbolic Execution
15mAbstract Interpretation of Temporal Safety Effects of Higher Order Programs
23mAnyDSL: A Partial Evaluation Framework for Programming High-Performance Libraries
19mSSA without Dominance for Higher-Order Programs