REVIEW 2 cited by
Complete Relational Logic for Infinite-Dimensional Quantum Programs with Unbounded Assertions
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
Complete Relational Logic for Infinite-Dimensional Quantum Programs with Unbounded Assertions
read the original abstract
We present sound and complete relational program logics for infinite-dimensional quantum and classical-quantum programs. The logics model assertions as self-adjoint unbounded linear relations, which simultaneously support quantitative and qualitative reasoning. Our main theoretical results include new convergence theorems and infinite-dimensional duality theorems for infinite-dimensional quantum states, which we use to establish completeness.
Forward citations
Cited by 2 Pith papers
-
Formal Verification of Continuous-Variable Quantum Programs
A sound and relatively complete Hoare logic for continuous-variable quantum programs, with polynomial assertions and an automated weakest-precondition calculator.
-
Hybrid Path-Sums for Hybrid Quantum Programs
Hybrid Path-Sums offer a new symbolic framework with rewriting rules and assertions to represent, simplify, and verify properties of hybrid quantum-classical programs.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.