{
  "annotation_id": "6da854c3-15a5-4372-86d7-7617227d6778",
  "date_created": "2026-03-02T18:02:13.749000Z",
  "date_modified": "2026-03-02T18:02:13.749000Z",
  "file_hash": "8bf74ddee2839d0bf177af0c18203575c0c6bab9350c5fc32655c2950f68fb48",
  "private": false,
  "record": {
    "abstract": "We develop a notion of predicate transformer and, in particular, the weakest\nprecondition, appropriate for quantum computation. We show that there is a\nStone-type duality between the usual state-transformer semantics and the\nweakest precondition semantics. Rather than trying to reduce quantum\ncomputation to probabilistic programming we develop a notion that is directly\ntaken from concepts used in quantum computation. The proof that weakest\npreconditions exist for completely positive maps follows immediately from the\nKraus representation theorem. As an example we give the semantics of Selinger\u0027s\nlanguage in terms of our weakest preconditions. We also cover some specific\nsituations and exhibit an interesting link with stabilizers.",
    "arxiv_id": "quant-ph/0501157",
    "authors": [
      "Ellie D\u0027Hondt",
      "Prakash Panangaden"
    ],
    "categories": [
      "quant-ph"
    ],
    "journal_ref": "Mathematical Structures in Computer Science, 2006",
    "title": "Quantum Weakest Preconditions",
    "url": "https://arxiv.org/abs/quant-ph/0501157"
  },
  "schema_id": "dorsal/arxiv",
  "source": {
    "execution_id": "63308f11-3cc1-4893-8607-15439a2210e2",
    "id": "arXiv Dataset IDs",
    "type": "Model",
    "variant": "snapshot-2026-03-01",
    "version": "0.1.0"
  },
  "user_id": 1000002
}