Adaptable Traces for Program Explanations
summary
Claim: program execution proof trees become readable explanations after systematic trace transformations that preserve proof content while drastically shrinking size. Method: a conservative call-by-named-value semantics produces named values, then three concrete operations hide/apply/factor transform DAG-shaped traces and replace environments with binding nodes. Result: a prototype filter/query engine and UI that shrinks the massive factorial of 6 trace into several user-controlled views; transformations succeed in producing succinct, informative explanations.
AI-written summary · about
chapters (20)
- 0:00Intro
- 0:32OUTLINE
- 1:35Object Language
- 2:31Why Named Values?
- 3:44Transforming Proof Trees to Traces
- 4:11Sharing Equivalent Nodes
- 4:40Removing Environments
- 5:11Tagging Bindings with Origin-Scope Pair
- 5:39Replacing Variable Lookups with Binding Nodes
- 6:23A Trace as an Explanation
- 7:19Operations on Traces
- 7:48Hiding Nodes
- 8:57Applying Judgments
- 9:33Factoring Subtraces
- 10:10A Query Language
- 11:01Applying Queries on Traces
- 12:00Complete Trace for a Program to find Factorial of 6
- 12:20Explanation for a Program to find Factorial of 6
- 13:12Another Explanation for Factorial of 6
- 13:49Conclusion
related talks
31mLiterate Tracing
12mAnswering Developer Questions with Annotated Agent-Discovered Program Traces
34mVisualising program execution
24mTowards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by(…)
26mTime-awareness in Object-exploration Tools: Toward In Situ Omniscient Debugging
21mEnhancing Proof Stability
56mMy Journey to the Dark Side: Under-Approximation, Incorrectness, Proof
30mVisualizing process evolution