Sulfur: Substitution Generation using a Logical Framework
summary
A Coq/Rocq plugin reimplements Autosubst’s costly asimpl by reflective tactic reification: it generates concrete de Bruijn-based syntax, translates terms into an explicit sigma-like language (with t_subs, SID and explicit composition), runs a Coq function to simplify it, and evaluates back. The simplifier is proven soundness w.r.t. evaluation, avoids rebuilding large proofs, and is noticeably faster than asimpl (asimpl once consumed >75% of typechecking time; authors estimate ~10× speedup but report no formal benchmarks). Current limits: single-sorted extrinsic syntax only and basic optimization.
AI-written summary · about
chapters (12)
- 0:00Sulfur project introduction
- 1:05Autosubst and binders
- 2:48Limitations of asimple tactic
- 3:32Sulfur’s efficiency key idea
- 4:54Concrete vs explicit syntax
- 7:03Signature-based language abstraction
- 8:08How asimple works
- 9:10Reflection benefits
- 9:52Future work benchmarks
- 10:35Multiple sorts challenges
- 11:37Completeness theorem
- 12:01Q&A
related talks
56mAutosubst 2: Reasoning with de Bruijn Terms and Substitutions
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
46mMechanizing Abstract Interpretation
16mPyrosome: Verified Compilation for Modular Metatheory
19mExtensible Metatheory Mechanization via Family Polymorphism
29mSemantic Transformation Framework for Rewriting Rules
30mAnalyzing Programs with SMT Solvers