A Formal Foundation for Symbolic Evaluation with Merging
summary
New formal symbolic semantics incorporates state merging and a parameterized symbolic factory and is mechanized in Lean, proving soundness, completeness, legality and reducibility with respect to a concrete lambda C semantics. A Lean reference evaluator (Leanette) is proven correct; an optimized Racket implementation (Rosette 4) is validated by solver-aided differential testing against Leanette. Sixteen published Rosette 3 client tools are ported to Rosette 4 and benchmarks show Rosette 4 matches or slightly improves Rosette 3 performance.
AI-written summary · about
chapters (25)
- 0:00Introduction
- 0:11Purpose
- 1:07Reusable
- 2:02Challenges
- 3:16Key Ideas
- 4:15Concrete Contributions
- 4:32Leannet
- 5:14Outline
- 6:51Simulate Value
- 8:08Simulate Operations
- 8:48Symbolic Equation
- 10:18Model
- 10:44Merging
- 11:29Symbolic Factory Interface
- 12:38correctness
- 13:19Symbolic completeness
- 13:58Partial correctness
- 14:23Key environments
- 14:40Reducibility states
- 16:23Research questions
- 16:36Reusability
- 17:18Generality
- 17:59Efficiency
- 18:40Conclusion
- 18:56Questions