Cover Image

Compiling by Proving: Language-Agnostic Automatic Optimization from Formal Semantics

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Zhao, Jianhong, Hildenbrandt, Everett, Conejero, Juan, Zhao, Yongwang
Format:	Preprint
Published:	2025
Subjects:	Programming Languages Computation and Language
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

K-CIRCT: A Layered, Composable, and Executable Formal Semantics for CIRCT Hardware IRs
by: Zhao, Jianhong, et al.
Published: (2024)

Linguine: A Natural-Language Programming Language with Formal Semantics and a Clean Compiler Pipeline
by: Hu, Lifan
Published: (2025)

Compilation as Multi-Language Semantics
by: Bowman, William J.
Published: (2025)

CktFormalizer: Autoformalization of Natural Language into Circuit Representations
by: Xiong, Jing, et al.
Published: (2026)

Pragmatics of Formally Verified Yet Efficient Static Analysis, in particular for Formally Verified Compilers
by: Monniaux, David
Published: (2024)

Algorithmic Language Models with Neurally Compiled Libraries
by: Saldyt, Lucas, et al.
Published: (2024)

Compilation Semantics for a Programming Language with Versions
by: Tanabe, Yudai, et al.
Published: (2023)

An In-Context Learning Agent for Formal Theorem-Proving
by: Thakur, Amitayush, et al.
Published: (2023)

LOOPer: A Learned Automatic Code Optimizer For Polyhedral Compilers
by: Merouani, Massinissa, et al.
Published: (2024)

From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs
by: Cao, Jialun, et al.
Published: (2025)

Reinforcement Learning from Compiler and Language Server Feedback
by: Zhang, Yifan, et al.
Published: (2025)

MappedTrace: Tracing Pointer Remotely with Compiler-generated Maps
by: Ma, Zhiyao, et al.
Published: (2025)

CompilerGPT: Leveraging Large Language Models for Analyzing and Acting on Compiler Optimization Reports
by: Pirkelbauer, Peter, et al.
Published: (2025)

Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs
by: Li, Guchan, et al.
Published: (2026)

From Algebraic Word Problem to Program: A Formalized Approach
by: Wiemerslage, Adam, et al.
Published: (2020)

Proving Confluence in the Confluence Framework with CONFident
by: Gutiérrez, Raúl, et al.
Published: (2023)

Automated Theorem Proving for Prolog Verification
by: Mesnard, Fred, et al.
Published: (2026)

Generation of Compiler Backends from Formal Models of Hardware
by: Smith, Gus Henry
Published: (2024)

A Formal Semantics of the GraalVM Intermediate Representation
by: Webb, Brae J., et al.
Published: (2021)

Developing a Modular Compiler for a Subset of a C-like Language
by: Dutta, Debasish, et al.
Published: (2025)

Meta Large Language Model Compiler: Foundation Models of Compiler Optimization
by: Cummins, Chris, et al.
Published: (2024)

Synthesizing Formal Semantics from Executable Interpreters
by: Liu, Jiangyi, et al.
Published: (2024)

Improving LLM Code Reasoning via Semantic Equivalence Self-Play with Formal Verification
by: Barone, Antonio Valerio Miceli, et al.
Published: (2026)

LLM-Agnostic Semantic Representation Attack
by: Lian, Jiawei, et al.
Published: (2026)

SAC-Opt: Semantic Anchors for Iterative Correction in Optimization Modeling
by: Zhang, Yansen, et al.
Published: (2025)

The Formal Semantics and Implementation of a Domain-Specific Language for Mixed-Initiative Dialogs
by: Rowland, Zachary S., et al.
Published: (2025)

SECOMP: Formally Secure Compilation of Compartmentalized C Programs
by: Thibault, Jérémy, et al.
Published: (2024)

AIOS Compiler: LLM as Interpreter for Natural Language Programming and Flow Programming of AI Agents
by: Xu, Shuyuan, et al.
Published: (2024)

An Optimizing Just-In-Time Compiler for Rotor
by: Trindade, João H., et al.
Published: (2024)

A Compiler for Operations on Relations with Bag Semantics
by: Dong, James, et al.
Published: (2025)

Automatic Functional Differentiation in JAX
by: Lin, Min
Published: (2023)

A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL
by: Xu, Qiyuan, et al.
Published: (2025)

OProver: A Unified Framework for Agentic Formal Theorem Proving
by: Ma, David, et al.
Published: (2026)

HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement
by: Hu, Jilin, et al.
Published: (2025)

Semantic Source Code Segmentation using Small and Large Language Models
by: Dahou, Abdelhalim, et al.
Published: (2025)

Non-Termination Proving: 100 Million LoC and Beyond
by: Vanegue, Julien, et al.
Published: (2025)

Scaling Optimization Over Uncertainty via Compilation
by: Cho, Minsung, et al.
Published: (2025)

Pattern Matching in AI Compilers and its Formalization (Extended Version)
by: Cutler, Joseph W., et al.
Published: (2024)

Random Variate Generation with Formal Guarantees
by: Saad, Feras A., et al.
Published: (2025)

Interaction Tree Semantics for RISC-V: Bridging Compiler and Hardware Verification
by: Kan, Shuanglong, et al.
Published: (2026)