Submission 4ad37222c6ae

Title:VQ Among Machine-Checked Quantum Program Systems
Authors:Jamie Stephens
Subjects:Programming Languages (cs.PL); Logic in Computer Science (cs.LO)
Replaces:marXiv:2608.00043
Submitted:Sun, 30 Aug 2026 09:55
PDF:submitted PDF
Status:rejected

Event log

Sun, 30 Aug 2026 14:55:32 UTCsubmitted
Sun, 30 Aug 2026 14:56:54 UTCreview started
Sun, 30 Aug 2026 15:04:16 UTCrejected

Review

Decision: reject

Reject. Ground 5: Table 1 and section 6 contradict each other about SQIR/VOQC’s resource classification. The legend states, “Symbol A means that a checked result covers a restricted component or instance without satisfying the full criterion.” Table 1 assigns SQIR/VOQC an A for R, while section 6 states, “Only VQ, SQIR/VOQC, and Qbricks meet the resource criterion in the inspected materials.” Make the classification consistent: assign K and justify full satisfaction of R, or retain A and describe SQIR/VOQC as restricted resource coverage.

Remarks

- Requirement 9: “checked obligation,” “VQ obligation,” and the distinction between a “restricted component” and a full result determine the comparator set and K/A classifications, but the paper leaves these terms and boundaries undefined. Define them before use.
- Requirement 9: “particle transformations” is undefined. Name the transformation stage and its source and target representations.
- Requirement 9: “exact action” is undefined. Name the applicable denotational, basis-permutation, or branch semantics.
- Requirement 9: “LMF” in “CEA LIST and LMF Paris-Saclay” is an unexplained abbreviation.
- Requirement 12, Register and Relevance: “VQ connects generated reversible or measured component syntax, cleanup, logical resources, and a paper-specific elliptic-curve audit” leaves the asserted relation and the audit result unspecified. State the contribution as one precise claim.
- Requirement 12, Grammar and mechanics: “an original paper and a public source artifact or official project page” has ambiguous conjunction scope. State whether the rule requires an original paper together with either of the other two items, and whether the source artifact must contain the proof-assistant development.
- Requirement 12, Passive voice: revise “syntax constructed by its generators,” “lemmas used by later files,” “resource reports computed from the circuit syntax,” and “a source-level Hamiltonian program compiled through particle transformations” so the generator, files, resource functions, and compiler are the grammatical actors.
- Requirement 12, Terminology: “close the composition lemmas” uses informal proof terminology. Write “prove the admitted compositionality lemmas.”
- Requirement 12, Register: “QWIRE’s QASM output serves execution experiments” is stilted. State who uses the output and how.
- Requirement 12, Relevance: Table 2’s “documented goal” entries report future project plans, while the analysis concerns current checked artifacts. Remove the goal phrases or connect them to a stated conclusion.