Compiling by Proving: Language-Agnostic Automatic Optimization from Formal Semantics. - Jianhong Zhao; Everett Hildenbrandt; Juan Conejero; Yongwang Zhao (CoRR, 2025)