Provingly Correct Optimisations on Intrinsically Typed Expressions (Extended Abstract)
summary
Implements dead binding elimination for intrinsically typed syntax trees by annotating each subexpression with a live-variable subcontext and using order-preserving subcontext embeddings to remove unused lets without renaming; evaluation remains total and the pipeline separates analysis (existential subcontext) from transformation. The implementation in Agda produces a semantics-preserving proof showing evaluating the optimized term equals evaluating the original, and the code plus extended abstract are available online.
AI-written summary · about