Imagen de Portada

Automating Equational Proofs in Dirac Notation

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	Xu, Yingte, Barthe, Gilles, Zhou, Li
Formato:	Preprint
Publicado:	2024
Materias:	Programming Languages
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

D-Hammer: Efficient Equational Reasoning for Labelled Dirac Notation
por: Xu, Yingte, et al.
Publicado: (2025)

Laws of Quantum Programming
por: Ying, Mingsheng, et al.
Publicado: (2024)

A Duality Theorem for Classical-Quantum States with Applications to Complete Relational Program Logics
por: Barthe, Gilles, et al.
Publicado: (2025)

(Dis)Proving Spectre Security with Speculation-Passing Style
por: Arranz-Olmos, Santiago, et al.
Publicado: (2025)

Agentic Proof Automation: A Case Study
por: Xu, Yichen, et al.
Publicado: (2026)

Critical Semantic Properties of Music Notation Datasets
por: Lepper, Markus, et al.
Publicado: (2024)

Decompiling for Constant-Time Analysis
por: Arranz-Olmos, Santiago, et al.
Publicado: (2025)

A Direct-Style Effect Notation for Sequential and Parallel Programs
por: Richter, David, et al.
Publicado: (2023)

The Jasmin Compiler Preserves Cryptographic Security
por: Arranz-Olmos, Santiago, et al.
Publicado: (2025)

Traq: Estimating the Quantum Cost of Classical Programs
por: Peduri, Anurudh, et al.
Publicado: (2025)

Automating Unrealizability Logic: Hoare-Style Proof Synthesis for Infinite Sets of Programs
por: Nagy, Shaan, et al.
Publicado: (2024)

Refactoring and Equivalence in Rust: Expanding the REM Toolchain with a Novel Approach to Automated Equivalence Proofs
por: Britton, Matthew, et al.
Publicado: (2026)

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

A Natural Formalized Proof Language
por: Xie, Lihan, et al.
Publicado: (2024)

Proof Repair across Quotient Type Equivalences
por: Viola, Cosmo, et al.
Publicado: (2023)

Adaptive Shielding via Parametric Safety Proofs
por: Feng, Yao, et al.
Publicado: (2025)

Asynchronous Global Protocols, Precisely: Full Proofs
por: Pischke, Kai, et al.
Publicado: (2025)

Mechanizing a Proof-Relevant Logical Relation for Timed Message-Passing Protocols
por: Zhang, Tesla, et al.
Publicado: (2025)

Incremental Proof Development in Dafny with Module-Based Induction
por: Ho, Son, et al.
Publicado: (2024)

Scenario-Based Proofs for Concurrent Objects [Extended Version]
por: Enea, Constantin, et al.
Publicado: (2023)

Mechanized Metatheory of Forward Reasoning for End-to-End Linearizability Proofs
por: Kent, Zachary, et al.
Publicado: (2025)

A Notation for Describing the Components of Library Information Systems.
por: Momenee, Karen
Publicado: (1982)

A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants
por: Bayazıt, Barış, et al.
Publicado: (2025)

Smooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs and Compilers
por: Conoly, Owen, et al.
Publicado: (2025)

Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report)
por: Paraskevopoulou, Zoe
Publicado: (2026)

The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs (Extended Version)
por: Schüssele, Frank, et al.
Publicado: (2025)

FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?
por: Ravi, Nikil, et al.
Publicado: (2026)

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

Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq
por: Gross, Jason, et al.
Publicado: (2023)

Symmetric Proofs of Parameterized Programs
por: Cheng, Ruotong, et al.
Publicado: (2026)

Coinductive Proofs for Temporal Hyperliveness
por: Correnson, Arthur, et al.
Publicado: (2025)

Unlocking the Power of Environment Assumptions for Unit Proofs
por: Priya, Siddharth, et al.
Publicado: (2024)

Pacing Types for Asynchronous Stream Equations
por: Kohn, Florian, et al.
Publicado: (2026)

ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations
por: Gu, Alex, et al.
Publicado: (2025)

MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data
por: Huang, Yinya, et al.
Publicado: (2024)

More Church-Rosser Proofs in BELUGA
por: Momigliano, Alberto, et al.
Publicado: (2024)

Automated Verification of Soundness of DNN Certifiers
por: Singh, Avaljot, et al.
Publicado: (2025)

Verification Algorithms for Automated Separation Logic Verifiers
por: Eilers, Marco, et al.
Publicado: (2024)

Automated Expected Cost Analysis for Quantum Programs
por: Moser, Georg, et al.
Publicado: (2026)

Cyclic Proofs in Hoare Logic and its Reverse
por: Brotherston, James, et al.
Publicado: (2025)