On the public citation graph
Quantum relational Hoare logic
0 signed · 92 inferred · view as graph
Inferred edges come from two machine sources: sweeps of open repository metadata (mostly SSRN and Zenodo), and a bulk OpenAlex citation snapshot. Every row below is labelled with the one it came from. Neither is a complete citation index — absence here is not evidence of absence.
Is this your work? Sign in with ORCID and put your name on the
claims that are yours.
Reference health. See whether every reference in this work resolves to a
known work and none has been retracted — and get a dated CiteStamped
badge you can embed.
What this work says
Outgoing claims: the papers this work cites, builds on, or argues with.
inferredcites →https://doi.org/10.1007/11761679_25openalex-snapshot
The Security of Triple Encryption and a Framework for Code-Based Game-Playing Proofs
inferredcites →https://doi.org/10.1007/978-3-642-10622-4_7openalex-snapshot
A Logic for Formal Verification of Quantum Programs
inferredcites →https://doi.org/10.1007/978-3-642-25385-0_3openalex-snapshot
Random Oracles in a Quantum World
inferredcites →https://doi.org/10.1007/978-3-642-29011-4_10openalex-snapshot
Quantum Proofs of Knowledge
inferredcites →https://doi.org/10.1007/978-3-642-32009-5_44openalex-snapshot
Secure Identity-Based Encryption in the Quantum Random Oracle Model
inferredcites →https://doi.org/10.1007/978-3-642-36742-7_33openalex-snapshot
Equivalence Checking of Quantum Protocols
inferredcites →https://doi.org/10.1007/978-3-642-54862-8_42openalex-snapshot
Verification of Concurrent Quantum Protocols by Equivalence Checking
inferredcites →https://doi.org/10.1007/978-3-662-46666-7_4openalex-snapshot
The Foundational Cryptography Framework
inferredcites →https://doi.org/10.1007/978-3-662-46803-6_25openalex-snapshot
Non-Interactive Zero-Knowledge Proofs in the Quantum Random Oracle Model
inferredcites →https://doi.org/10.1007/978-3-662-48899-7_27openalex-snapshot
Relational Reasoning via Probabilistic Coupling
inferredcites →https://doi.org/10.1007/bf00417500openalex-snapshot
Quantum generalizations of Bell's inequality
inferredcites →https://doi.org/10.1007/s00145-001-0014-7openalex-snapshot
Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption)
inferredcites →https://doi.org/10.1007/s00145-002-0204-yopenalex-snapshot
RSA-OAEP Is Secure under the RSA Assumption
inferredcites →https://doi.org/10.1016/j.entcs.2006.04.003openalex-snapshot
Reasoning About Imperative Quantum Programs
inferredcites →https://doi.org/10.1016/j.entcs.2011.01.016openalex-snapshot
Verification of Quantum Protocols with a Probabilistic Model-Checker
inferredcites →https://doi.org/10.1016/j.tcs.2007.06.011openalex-snapshot
Proof rules for the correctness of quantum programs
inferredcites →https://doi.org/10.1016/j.tcs.2014.05.025openalex-snapshot
Quantum cryptography: Public key distribution and coin tossing
inferredcites →https://doi.org/10.1017/s0960129506005251openalex-snapshot
Quantum weakest preconditions
inferredcites →https://doi.org/10.1103/physrevlett.23.880openalex-snapshot
Proposed Experiment to Test Local Hidden-Variable Theories
inferredcites →https://doi.org/10.1103/physrevlett.85.441openalex-snapshot
Simple Proof of Security of the BB84 Quantum Key Distribution Protocol
inferredcites →https://doi.org/10.1109/focs.2012.37openalex-snapshot
How to Construct Quantum Random Functions
inferredcites →https://doi.org/10.1109/focs.2014.57openalex-snapshot
Quantum Attacks on Classical Proof Systems: The Hardness of Quantum Rewinding
inferredcites →https://doi.org/10.1109/sp.2006.1openalex-snapshot
A computationally sound mechanized prover for security protocols
inferredcites →https://doi.org/10.1109/tit.1983.1056650openalex-snapshot
On the security of public key protocols
inferredcites →https://doi.org/10.1137/060670997openalex-snapshot
Zero-Knowledge against Quantum Attacks
inferredcites →https://doi.org/10.1145/1480881.1480894openalex-snapshot
Formal certification of code-based cryptographic proofs
inferredcites →https://doi.org/10.1145/2049706.2049708openalex-snapshot
Floyd--hoare logic for quantum programs
inferredcites →https://doi.org/10.1145/2817206openalex-snapshot
Revocable Quantum Timed-Release Encryption
inferredcites →https://doi.org/10.1145/3009837.3009896openalex-snapshot
Coupling proofs are probabilistic product programs
inferredcites →https://doi.org/10.1145/3291619openalex-snapshot
Verification tool for quantum relational Hoare Logic
inferredcites →https://doi.org/10.1145/964001.964003openalex-snapshot
Simple relational correctness proofs for static analyses and program transformations
What points at this work
Incoming claims: where this work appears in other papers’ reference lists and arguments.
inferred← citeshttps://doi.org/10.1002/9781119836728.ch10openalex-snapshot
Quantum Protocols for Hash‐Based Blockchain
inferred← citeshttps://doi.org/10.1007/978-3-030-64837-4_11openalex-snapshot
Post-Quantum Verification of Fujisaki-Okamoto
inferred← citeshttps://doi.org/10.1007/978-3-031-50521-8_8openalex-snapshot
Local Reasoning About Probabilistic Behaviour for Classical–Quantum Programs
inferred← citeshttps://doi.org/10.1007/978-3-031-65633-0_22openalex-snapshot
Approximate Relational Reasoning for Quantum Programs
inferred← citeshttps://doi.org/10.1007/978-3-031-66997-2_8openalex-snapshot
Formalizing Coppersmith’s Method in Isabelle/HOL
inferred← citeshttps://doi.org/10.1007/978-3-031-68379-4_12openalex-snapshot
Formally Verifying Kyber
inferred← citeshttps://doi.org/10.1007/978-3-031-98685-7_3openalex-snapshot
D-Hammer: Efficient Equational Reasoning for Labelled Dirac Notation
inferred← citeshttps://doi.org/10.1007/978-3-032-22626-6_4openalex-snapshot
Satisfaction-Based Probabilistic Hoare Logic with While Loop: Weakest Precondition and Relative Completeness
inferred← citeshttps://doi.org/10.1007/s00165-019-00501-3openalex-snapshot
Fifty years of Hoare’s logic
inferred← citeshttps://doi.org/10.1007/s10817-023-09689-9openalex-snapshot
A Formalization of the CHSH Inequality and Tsirelson’s Upper-bound in Isabelle/HOL
inferred← citeshttps://doi.org/10.1007/s11128-026-05296-wopenalex-snapshot
Weakest precondition calculus and relative completeness of satisfaction-based quantum Hoare logic
inferred← citeshttps://doi.org/10.1007/s11390-021-1637-9openalex-snapshot
Symbolic Reasoning About Quantum Circuits in Coq
inferred← citeshttps://doi.org/10.1016/b978-0-44-315942-8.00016-2openalex-snapshot
Quantum Hoare logic
inferred← citeshttps://doi.org/10.1016/b978-0-44-315942-8.00018-6openalex-snapshot
Verification of quantum programs
inferred← citeshttps://doi.org/10.1016/j.ic.2026.105417openalex-snapshot
A practical quantum Hoare logic with classical variables, I
inferred← citeshttps://doi.org/10.1016/j.tcs.2019.08.026openalex-snapshot
Strassen's theorem for quantum couplings
inferred← citeshttps://doi.org/10.1073/pnas.2218775120openalex-snapshot
A formally certified end-to-end implementation of Shor’s factorization algorithm
inferred← citeshttps://doi.org/10.1109/jetcas.2022.3205174openalex-snapshot
Advances in Quantum Computation and Quantum Technologies: A Design Automation Perspective
inferred← citeshttps://doi.org/10.1109/lics.2019.8785779openalex-snapshot
Quantum Hoare Logic with Ghost Variables
inferred← citeshttps://doi.org/10.1109/lics52264.2021.9470673openalex-snapshot
A Quantum Interpretation of Bunched Logic & Quantum Separation Logic
inferred← citeshttps://doi.org/10.1109/lics65433.2025.00072openalex-snapshot
Complete Quantum Relational Hoare Logics from Optimal Transport Duality
inferred← citeshttps://doi.org/10.1109/q-se59154.2023.00014openalex-snapshot
QChecker: Detecting Bugs in Quantum Programs via Static Analysis
inferred← citeshttps://doi.org/10.1109/qsw59989.2023.00029openalex-snapshot
QIn: Enabling Formal Methods to Deal with Quantum Circuits
inferred← citeshttps://doi.org/10.1109/sp46214.2022.9833800openalex-snapshot
A Logic and an Interactive Prover for the Computational Post-Quantum Security of Protocols
inferred← citeshttps://doi.org/10.1142/s0218126624501123openalex-snapshot
Formalizing the Semantics of a Classical-Quantum Imperative Language in Coq
inferred← citeshttps://doi.org/10.1145/3314221.3314584openalex-snapshot
An applied quantum Hoare logic
inferred← citeshttps://doi.org/10.1145/3371072openalex-snapshot
The next 700 relational program logics
inferred← citeshttps://doi.org/10.1145/3371089openalex-snapshot
Relational proofs for quantum programs
inferred← citeshttps://doi.org/10.1145/3428218openalex-snapshot
Projection-based runtime assertions for testing and debugging Quantum programs
inferred← citeshttps://doi.org/10.1145/3434286openalex-snapshot
On algebraic abstractions for concurrent separation logics
inferred← citeshttps://doi.org/10.1145/3450144openalex-snapshot
Definitions and Analysis of Quantum E-voting Protocols
inferred← citeshttps://doi.org/10.1145/3453483.3454061openalex-snapshot
Quantum abstract interpretation
inferred← citeshttps://doi.org/10.1145/3456877openalex-snapshot
Quantum Hoare Logic with Classical Variables
inferred← citeshttps://doi.org/10.1145/3460120.3484567openalex-snapshot
EasyPQC: Verifying Post-Quantum Cryptography
inferred← citeshttps://doi.org/10.1145/3519939.3523713openalex-snapshot
Algebraic reasoning of Quantum programs via non-idempotent Kleene algebra
inferred← citeshttps://doi.org/10.1145/3527316openalex-snapshot
On incorrectness logic for Quantum programs
inferred← citeshttps://doi.org/10.1145/3571222openalex-snapshot
CoqQ: Foundational Verification of Quantum Programs
inferred← citeshttps://doi.org/10.1145/3582016.3582039openalex-snapshot
Verification of Nondeterministic Quantum Programs
inferred← citeshttps://doi.org/10.1145/3624483openalex-snapshot
Formal Verification of Quantum Programs: Theory, Tools, and Challenges
inferred← citeshttps://doi.org/10.1145/3703595.3705887openalex-snapshot
Formalizing the One-Way to Hiding Theorem
inferred← citeshttps://doi.org/10.1145/3704876openalex-snapshot
A Quantitative Probabilistic Relational Hoare Logic
inferred← citeshttps://doi.org/10.1145/3704878openalex-snapshot
Automating Equational Proofs in Dirac Notation
inferred← citeshttps://doi.org/10.1145/3704889openalex-snapshot
Coinductive Proofs for Temporal Hyperliveness
inferred← citeshttps://doi.org/10.1145/3720433openalex-snapshot
QbC: Quantum Correctness by Construction
inferred← citeshttps://doi.org/10.1145/3729293openalex-snapshot
Efficient Formal Verification of Quantum Error Correcting Programs
inferred← citeshttps://doi.org/10.1145/3763153openalex-snapshot
Scalable Equivalence Checking and Verification of Shallow Quantum Circuits
inferred← citeshttps://doi.org/10.1145/3763157openalex-snapshot
Embedding Quantum Program Verification into Dafny
inferred← citeshttps://doi.org/10.1145/3776658openalex-snapshot
An Expressive Assertion Language for Quantum Programs
inferred← citeshttps://doi.org/10.1145/3808314openalex-snapshot
Hybrid Path-Sums for Hybrid Quantum Programs
inferred← citeshttps://doi.org/10.1145/3815573openalex-snapshot
Reasoning about Parameterized Recursive Quantum Programs with Ancilla Data and Probabilistic Control
inferred← citeshttps://doi.org/10.1145/3843234openalex-snapshot
Refinement Orders for Quantum Programs
inferred← citeshttps://doi.org/10.2139/ssrn.7361162openalex-snapshot
Local Reasoning about Probabilistic Behaviour for Classical-Quantum Programs
inferred← citeshttps://doi.org/10.2200/s01014ed1v01y202005cac051openalex-snapshot
Quantum Computer Systems: Research for Noisy Intermediate-Scale Quantum Computers
inferred← citeshttps://doi.org/10.70675/adcfd403z5566z460dz9591zebb0e4f5a766openalex-snapshot
Principles of program verification for arbitrary monadic effects
showing the first 58 of 59 · page through all 59
Editorial review for independent work. ICSAC — the Institute for Complexity
Science and Advanced Computing — runs a structured editorial panel for researchers
publishing outside journals, and publishes on CiteStamp rails. Submission is free
and goes through ORCID: icsacinstitute.org/submit.