Compiling by Proving: Language-Agnostic Automatic Optimization from Formal Semantics
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Empowering In-Browser Deep Learning Inference on Edge Devices with Just-in-Time Kernel Optimizations
Web is increasingly becoming the primary platform to deliver AI services onto edge devices, making in-browser deep learning (DL) inference more prominent. Nevertheless, the heterogeneity of edge devices, combined with th…
A Framework for Compiling High Quality Knowledge Resources From Raw Corpora
The identification of various types of relations is a necessary step to allow computers to understand natural language text. In particular, the clarification of relations between predicates and their arguments is essenti…
Dependency ParsingMachine TranslationRelation ExtractionVocal Bursts Intensity PredictionCOMPILING: A Benchmark Dataset for Chinese Complexity Controllable Definition Generation
The definition generation task aims to generate a word's definition within a specific context automatically. However, owing to the lack of datasets for different complexities, the definitions produced by models tend to k…
Reproducible Science with LaTeX
This paper proposes a procedure to execute external source codes from a LaTeX document and include the calculation outputs in the resulting Portable Document Format (pdf) file automatically. It integrates programming too…
Efficient and practical quantum compiler towards multi-qubit systems with deep reinforcement learning
Efficient quantum compiling tactics greatly enhance the capability of quantum computers to execute complicated quantum algorithms. Due to its fundamental importance, a plethora of quantum compilers has been designed in p…
Deep Reinforcement LearningQ-Learningreinforcement-learningReinforcement Learning (RL)