論文の概要: BI-based Reasoning about Quantum Programs with Heap Manipulations

• arxiv url: http://arxiv.org/abs/2409.10153v1
• Date: Mon, 16 Sep 2024 10:34:45 GMT
• ステータス: 処理完了
• システム内更新日: 2024-09-17 16:00:03.463851
• Title: BI-based Reasoning about Quantum Programs with Heap Manipulations
• Title（参考訳）: BIに基づくヒープ操作による量子プログラムの推論
• Authors: Bonan Su, Li Zhou, Yuan Feng, Mingsheng Ying,
• Abstract要約: ヒープ操作を伴う量子プログラミング言語Q While-hpのセマンティクスについて述べる。 我々は,意味を分離するための解釈を含む,BIスタイルの量子論理を開発する。 次に、この量子BIスタイルの論理をアサーション言語として採用し、ヒープ制御量子プログラムを推論する。
• 参考スコア（独自算出の注目度）: 5.744265100221585
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We provide well-founded semantics for a quantum programming language Qwhile-hp with heap manipulations, where allocation statements follow a dirty pattern, meaning that newly allocated qubits can nondeterministically assume arbitrary initial states. To thoroughly characterize heap manipulations in the quantum setting, we develop a quantum BI-style logic that includes interpretations for separating implication ($-\mkern-3mu*$) and separating conjunction ($*$). We then adopt this quantum BI-style logic as an assertion language to reason about heap-manipulated quantum programs and present a quantum separation logic which is sound and relatively complete. Finally, we apply our framework to verify the correctness of various practical quantum programs and to prove the correct usage of dirty ancilla qubits.
• Abstract（参考訳）: 量子プログラミング言語Q While-hpにヒープ操作を施したセマンティクスを提供する。そこでは、割り当て文は汚いパターンに従っており、新たに割り当てられたキュービットは、任意初期状態を非決定的に仮定することができる。 量子環境でのヒープ操作を徹底的に特徴づけるために、含意を分離し(−\mkern-3mu*$)、接続を分離する(*$)という解釈を含む量子BIスタイルの論理を開発した。 次に、この量子BIスタイルの論理をアサーション言語として採用し、ヒープ制御された量子プログラムを推論し、健全で比較的完全である量子分離論理を提示する。 最後に,本フレームワークを用いて,各種量子プログラムの正当性を検証し,汚いアンシラ量子ビットの正当性を証明する。

関連論文リスト

• Quantum process tomography of continuous-variable gates using coherent states [49.299443295581064]
  ボソニックモード超伝導回路におけるコヒーレント状態量子プロセストモグラフィ(csQPT)の使用を実証する。 符号化量子ビット上の変位とSNAP演算を用いて構築した論理量子ゲートを特徴付けることにより,本手法の結果を示す。
  論文  参考訳（メタデータ） (2023-03-02T18:08:08Z)
• Verification of Nondeterministic Quantum Programs [1.9302781323430196]
  非決定論的選択は、実装の詳細を指定せずにプログラムの振る舞いを記述する方法を提供する有用なプログラム構成である。 非決定性は量子プログラミングにも導入され、非決定性量子プログラムの終了は広く分析されてきた。
  論文  参考訳（メタデータ） (2023-02-15T22:37:23Z)
• Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs [6.2147758224415055]
  フーア論理(ホーアりょうり、英: Hoare logic)は、コンピュータプログラムの静的解析において強力な手法である。 完全な量子抽象解釈は、量子ホア論理と量子不正確な論理を誘導することを示す。
  論文  参考訳（メタデータ） (2022-06-28T05:49:55Z)
• Birkhoff-von Neumann Quantum Logic as an Assertion Language for Quantum Programs [1.1878820609988696]
  量子変数を持つ一階述語論理は、量子プログラムの様々な性質を特定し、推論するためのアサーション言語として必要とされる。 本稿では,Birkhoff-von Neumann量子論理を量子変数上の普遍的および存在的量子化器を用いて一階拡張する。
  論文  参考訳（メタデータ） (2022-05-04T08:57:44Z)
• LQP: The Dynamic Logic of Quantum Information [77.34726150561087]
  本稿では,複合量子システムにおける情報フローの推論のための動的論理形式について紹介する。 本稿では,この論理の文法,関係意味論,音響証明システムについて述べる。 アプリケーションとしては,テレポーテーションプロトコルと標準量子秘密共有プロトコルに対して,正式な正当性を与えるために,我々のシステムを利用する。
  論文  参考訳（メタデータ） (2021-10-04T12:20:23Z)
• The Logic of Quantum Programs [77.34726150561087]
  本稿では,量子プログラムにおける情報フローの論理計算について述べる。 特に、複素量子系における量子測定、ユニタリ進化、絡み合いを扱うことができる動的論理を導入する。
  論文  参考訳（メタデータ） (2021-09-14T16:08:37Z)
• Depth-efficient proofs of quantumness [77.34726150561087]
  量子性の証明は、古典的検証器が信頼できない証明器の量子的利点を効率的に証明できる挑戦応答プロトコルの一種である。 本稿では、証明者が量子回路を一定深度でしか実行できない量子性構成の証明を2つ与える。
  論文  参考訳（メタデータ） (2021-07-05T17:45:41Z)
• Facial Expression Recognition on a Quantum Computer [68.8204255655161]
  量子機械学習手法を用いて表情認識の可能な解を示す。 適切に定義された量子状態の振幅に符号化されたグラフの隣接行列を操作する量子回路を定義する。
  論文  参考訳（メタデータ） (2021-02-09T13:48:00Z)
• A Quantum Interpretation of Bunched Logic for Quantum Separation Logic [22.507329566323982]
  プリコンディションとポストコンディションは、量子状態を記述するBI式である。 量子ワンタイムパッドとシークレット共有のセキュリティを証明するロジックを実践する。
  論文  参考訳（メタデータ） (2021-01-30T22:24:36Z)
• Quantum Hoare logic with classical variables [3.1181601933418897]
  古典変数と量子変数の両方を含む簡単な時相言語に対して量子ホア論理を提案する。 古典量子状態とそれに対応するアサーションの新たな定義により、論理体系は非常に単純であり、古典的プログラムの伝統的なホア論理と類似している。
  論文  参考訳（メタデータ） (2020-08-15T23:56:18Z)
• PBS-Calculus: A Graphical Language for Coherent Control of Quantum Computations [77.34726150561087]
  本稿では,量子演算のコヒーレント制御を含む量子計算を表現・推論するためにPBS計算を導入する。 我々はこの言語に方程式理論を加え、それが健全で完備であることが証明された。 我々は、制御された置換の実装やループのアンロールのようなアプリケーションを考える。
  論文  参考訳（メタデータ） (2020-02-21T16:15:58Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。