Compiling by Proving: Language-Agnostic Automatic Optimization from Formal Semantics
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866918148672847872 |
|---|---|
| author | Zhao, Jianhong Hildenbrandt, Everett Conejero, Juan Zhao, Yongwang |
| author_facet | Zhao, Jianhong Hildenbrandt, Everett Conejero, Juan Zhao, Yongwang |
| contents | Verification proofs encode complete program behavior, yet we discard them after checking correctness. We present compiling by proving, a paradigm that transforms these proofs into optimized execution rules. By constructing All-Path Reachability Proofs through symbolic execution and compiling their graph structure, we consolidate many semantic rewrites into single rules while preserving correctness by construction. We implement this as a language-agnostic extension to the K framework. Evaluation demonstrates performance improvements across different compilation scopes: opcode-level optimizations show consistent speedups, while whole-program compilation achieves orders of magnitude greater performance gains. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_21793 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Compiling by Proving: Language-Agnostic Automatic Optimization from Formal Semantics Zhao, Jianhong Hildenbrandt, Everett Conejero, Juan Zhao, Yongwang Programming Languages Computation and Language Verification proofs encode complete program behavior, yet we discard them after checking correctness. We present compiling by proving, a paradigm that transforms these proofs into optimized execution rules. By constructing All-Path Reachability Proofs through symbolic execution and compiling their graph structure, we consolidate many semantic rewrites into single rules while preserving correctness by construction. We implement this as a language-agnostic extension to the K framework. Evaluation demonstrates performance improvements across different compilation scopes: opcode-level optimizations show consistent speedups, while whole-program compilation achieves orders of magnitude greater performance gains. |
| title | Compiling by Proving: Language-Agnostic Automatic Optimization from Formal Semantics |
| topic | Programming Languages Computation and Language |
| url | https://arxiv.org/abs/2509.21793 |