Buchumschlag

Pyrosome: Verified Compilation for Modular Metatheory

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Jamner, Dustin, Kammer, Gabriel, Nag, Ritam, Chlipala, Adam
Format:	Preprint
Veröffentlicht:	2025
Schlagworte:	Programming Languages
Online-Zugang:	Acceder al recurso
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!

Ähnliche Einträge

Smooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs and Compilers
von: Conoly, Owen, et al.
Veröffentlicht: (2025)

Accelerating Verified-Compiler Development with a Verified Rewriting Engine
von: Gross, Jason, et al.
Veröffentlicht: (2022)

Mechanized Metatheory of Forward Reasoning for End-to-End Linearizability Proofs
von: Kent, Zachary, et al.
Veröffentlicht: (2025)

Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq
von: Gross, Jason, et al.
Veröffentlicht: (2023)

Causality and Semantic Separation
von: Zhang, Anna, et al.
Veröffentlicht: (2026)

Testing, Credible Compilation, and Verification in the Axon Verified Compiler in Lean and Claude Code
von: Rinard, Martin
Veröffentlicht: (2026)

Compilation of Modular and General Sparse Workspaces
von: Zhang, Genghan, et al.
Veröffentlicht: (2024)

End-to-end Compositional Verification of Program Safety through Verified and Verifying Compilation
von: Wu, Jinhua, et al.
Veröffentlicht: (2025)

RustCompCert: A Verified and Verifying Compiler for a Sequential Subset of Rust
von: Wu, Jinhua, et al.
Veröffentlicht: (2026)

A Verified Compiler for Quantum Simulation
von: Li, Liyi, et al.
Veröffentlicht: (2025)

Outcome Logic: A Unified Approach to the Metatheory of Program Logics with Branching Effects
von: Zilberstein, Noam
Veröffentlicht: (2024)

Towards Verified Compilation of Floating-point Optimization in Scientific Computing Programs
von: Tekriwal, Mohit, et al.
Veröffentlicht: (2025)

Verifying Peephole Rewriting In SSA Compiler IRs
von: Bhat, Siddharth, et al.
Veröffentlicht: (2024)

Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report)
von: Paraskevopoulou, Zoe
Veröffentlicht: (2026)

Tenspiler: A Verified Lifting-Based Compiler for Tensor Operations (Extended Version)
von: Qiu, Jie, et al.
Veröffentlicht: (2024)

Pragmatics of Formally Verified Yet Efficient Static Analysis, in particular for Formally Verified Compilers
von: Monniaux, David
Veröffentlicht: (2024)

Modular Compilation for Quantum Chiplet Architectures
von: Jeng, Mingyoung Jessica, et al.
Veröffentlicht: (2025)

Foundational Verification of Smart Contracts through Verified Compilation
von: Sjöberg, Vilhelm, et al.
Veröffentlicht: (2024)

Securing Cryptographic Software via Typed Assembly Language (Extended Version)
von: Song, Shixin, et al.
Veröffentlicht: (2025)

Developing a Modular Compiler for a Subset of a C-like Language
von: Dutta, Debasish, et al.
Veröffentlicht: (2025)

Meta Large Language Model Compiler: Foundation Models of Compiler Optimization
von: Cummins, Chris, et al.
Veröffentlicht: (2024)

The CoCompiler: DSL Lifting via Relational Compilation
von: Spargo, Naomi, et al.
Veröffentlicht: (2025)

Compiling with Arrays
von: Richter, David, et al.
Veröffentlicht: (2024)

Verified VCG and Verified Compiler for Dafny
von: Nezamabadi, Daniel, et al.
Veröffentlicht: (2025)

Quantitative Comparison of Credible Compilation and Verification In Coding Agent Compiler Development
von: Rinard, Martin
Veröffentlicht: (2026)

CompilerGPT: Leveraging Large Language Models for Analyzing and Acting on Compiler Optimization Reports
von: Pirkelbauer, Peter, et al.
Veröffentlicht: (2025)

Compilation as Multi-Language Semantics
von: Bowman, William J.
Veröffentlicht: (2025)

Compiling Gradual Types with Evidence
von: Romero, José Luis, et al.
Veröffentlicht: (2025)

Partial Evaluation, Whole-Program Compilation
von: Fallin, Chris, et al.
Veröffentlicht: (2024)

Denotation-based Compositional Compiler Verification
von: Cheng, Zhang, et al.
Veröffentlicht: (2024)

An Optimizing Just-In-Time Compiler for Rotor
von: Trindade, João H., et al.
Veröffentlicht: (2024)

Verified Code Transpilation with LLMs
von: Bhatia, Sahil, et al.
Veröffentlicht: (2024)

A Lightweight Method for Generating Multi-Tier JIT Compilation Virtual Machine in a Meta-Tracing Compiler Framework
von: Izawa, Yusuke, et al.
Veröffentlicht: (2025)

Prime Path Coverage in the GNU Compiler Collection
von: Kvalsvik, Jørgen
Veröffentlicht: (2025)

Cyclotron: Compilation of Recurrences to Distributed and Systolic Architectures
von: Sundram, Shiv, et al.
Veröffentlicht: (2025)

Macro-embedding Compiler Intermediate Languages in Racket
von: Bowman, William J.
Veröffentlicht: (2025)

Compiling the Mimosa programming language to RTOS tasks
von: Huber, Nikolaus, et al.
Veröffentlicht: (2025)

Meta-compilation of Baseline JIT Compilers with Druid
von: Palumbo, Nahuel, et al.
Veröffentlicht: (2025)

Scaling Optimization Over Uncertainty via Compilation
von: Cho, Minsung, et al.
Veröffentlicht: (2025)

E-Graphs as a Persistent Compiler Abstraction
von: Merckx, Jules, et al.
Veröffentlicht: (2026)