Cover Image

Denotation-based Compositional Compiler Verification

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Cheng, Zhang, Wu, Jiyang, Wang, Di, Cao, Qinxiang
Format:	Preprint
Published:	2024
Subjects:	Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

A Coq Library of Sets for Teaching Denotational Semantics
by: Cao, Qinxiang, et al.
Published: (2024)

Encode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic
by: Wu, Shushu, et al.
Published: (2025)

A Denotational Semantics for Quantum Loops
by: Assolini, Nicola, et al.
Published: (2025)

A Formal Framework for Naturally Specifying and Verifying Sequential Algorithms
by: Yang, Chengxi, et al.
Published: (2025)

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

Abstracting Denotational Interpreters
by: Graf, Sebastian, et al.
Published: (2024)

C*: Unifying Programming and Verification in C
by: Cao, Yiyuan, et al.
Published: (2025)

A Natural Formalized Proof Language
by: Xie, Lihan, et al.
Published: (2024)

Towards General Loop Invariant Generation: A Benchmark of Programs with Memory Manipulation
by: Liu, Chang, et al.
Published: (2023)

Denotational reasoning for asynchronous multiparty session types
by: McDermott, Dylan, et al.
Published: (2026)

QCP: A Practical Separation Logic-based C Program Verification Tool
by: Wu, Xiwei, et al.
Published: (2025)

Quantitative Comparison of Credible Compilation and Verification In Coding Agent Compiler Development
by: Rinard, Martin
Published: (2026)

Denotational Correctness of Forward-Mode Automatic Differentiation for Iteration and Recursion
by: Vákár, Matthijs
Published: (2020)

Denotational Foundations for Expected Cost Analysis
by: de Amorim, Pedro H. Azevedo
Published: (2024)

Denotational Semantics for Probabilistic and Concurrent Programs
by: Zilberstein, Noam, et al.
Published: (2025)

Wiring the Pi-calculus to Denotational Semantics
by: Sakayori, Ken, et al.
Published: (2026)

Testing, Credible Compilation, and Verification in the Axon Verified Compiler in Lean and Claude Code
by: Rinard, Martin
Published: (2026)

Towards a Higher-Order Bialgebraic Denotational Semantics
by: Goncharov, Sergey, et al.
Published: (2026)

Denotational Semantics of Gradual Typing using Synthetic Guarded Domain Theory (Extended Version)
by: Giovannini, Eric, et al.
Published: (2024)

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

The Denotational Semantics of SSA
by: Ghalayini, Jad Elkhaleq, et al.
Published: (2024)

Stellis: A Strategy Language for Purifying Separation Logic Entailments
by: Wang, Zhiyi, et al.
Published: (2025)

Foundations of Digital Circuits: Denotation, Operational, and Algebraic Semantics
by: Kaye, George
Published: (2025)

Secure Composition of Robust and Optimising Compilers
by: Kruse, Matthis, et al.
Published: (2023)

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

Compositional Quantum Control Flow with Efficient Compilation in Qunity
by: Mints, Mikhail, et al.
Published: (2025)

A Complete Theory of Sequential Digital Circuits: Denotational, Operational and Algebraic Semantics
by: Ghica, Dan R., et al.
Published: (2022)

CompilerDream: Learning a Compiler World Model for General Code Optimization
by: Deng, Chaoyi, et al.
Published: (2024)

The CoCompiler: DSL Lifting via Relational Compilation
by: Spargo, Naomi, et al.
Published: (2025)

E-Graphs as a Persistent Compiler Abstraction
by: Merckx, Jules, et al.
Published: (2026)

Compiling with Arrays
by: Richter, David, et al.
Published: (2024)

Compilation of Modular and General Sparse Workspaces
by: Zhang, Genghan, et al.
Published: (2024)

PolyVer: A Compositional Approach for Polyglot System Modeling and Verification
by: Chen, Pei-Wei, et al.
Published: (2025)

RustCompCert: A Verified and Verifying Compiler for a Sequential Subset of Rust
by: Wu, Jinhua, et al.
Published: (2026)

Compiling the Mimosa programming language to RTOS tasks
by: Huber, Nikolaus, et al.
Published: (2025)

Cyclotron: Compilation of Recurrences to Distributed and Systolic Architectures
by: Sundram, Shiv, et al.
Published: (2025)

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

Compositional Neural-Cyber-Physical System Verification in the Interactive Theorem Prover of Your Choice
by: Daggitt, Matthew L., et al.
Published: (2026)

AwareCompiler: Agentic Context-Aware Compiler Optimization via a Synergistic Knowledge-Data Driven Framework
by: Lin, Hongyu, et al.
Published: (2025)

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