論文の概要: A Quantum Interpretation of Bunched Logic for Quantum Separation Logic
- arxiv url: http://arxiv.org/abs/2102.00329v1
- Date: Sat, 30 Jan 2021 22:24:36 GMT
- ステータス: 処理完了
- システム内更新日: 2023-04-13 06:55:36.108188
- Title: A Quantum Interpretation of Bunched Logic for Quantum Separation Logic
- Title（参考訳）: 量子分離論理のための束論理の量子解釈
- Authors: Li Zhou, Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu
- Abstract要約: プリコンディションとポストコンディションは、量子状態を記述するBI式である。
量子ワンタイムパッドとシークレット共有のセキュリティを証明するロジックを実践する。
- 参考スコア（独自算出の注目度）: 22.507329566323982
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We propose a model of the substructural logic of Bunched Implications (BI)
that is suitable for reasoning about quantum states. In our model, the
separating conjunction of BI describes separable quantum states. We develop a
program logic where pre- and post-conditions are BI formulas describing quantum
states -- the program logic can be seen as a counterpart of separation logic
for imperative quantum programs. We exercise the logic for proving the security
of quantum one-time pad and secret sharing, and we show how the program logic
can be used to discover a flaw in Google Cirq's tutorial on the Variational
Quantum Algorithm (VQA).
- Abstract（参考訳）: 本稿では,量子状態の推論に適した束縛的意味論(bi)のサブストラクショナル論理のモデルを提案する。
我々のモデルでは、BIの分離結合は分離可能な量子状態を記述する。
我々は,プリ条件とポスト条件が量子状態を記述するbi公式であるプログラム論理を開発する -- プログラム論理は命令型量子プログラムの分離論理の対として見ることができる。
我々は,量子ワンタイムパッドとシークレット共有の安全性を証明するための論理を実践し,プログラム論理がgoogle cirqの変分量子アルゴリズム(vqa)に関するチュートリアルにおいて,その欠陥の発見にどのように利用できるかを示す。
関連論文リスト
- BI-based Reasoning about Quantum Programs with Heap Manipulations [5.744265100221585]
ヒープ操作を伴う量子プログラミング言語Q While-hpのセマンティクスについて述べる。
我々は,意味を分離するための解釈を含む,BIスタイルの量子論理を開発する。
次に、この量子BIスタイルの論理をアサーション言語として採用し、ヒープ制御量子プログラムを推論する。
論文 参考訳（メタデータ） (2024-09-16T10:34:45Z) - Quantum process tomography of continuous-variable gates using coherent
states [49.299443295581064]
ボソニックモード超伝導回路におけるコヒーレント状態量子プロセストモグラフィ(csQPT)の使用を実証する。
符号化量子ビット上の変位とSNAP演算を用いて構築した論理量子ゲートを特徴付けることにより,本手法の結果を示す。
論文 参考訳（メタデータ） (2023-03-02T18:08:08Z) - Compilation of algorithm-specific graph states for quantum circuits [55.90903601048249]
本稿では,高レベル言語で記述された量子回路から,アルゴリズム固有のグラフ状態を作成する量子回路コンパイラを提案する。
この計算は、このグラフ状態に関する一連の非パウリ測度を用いて実装することができる。
論文 参考訳（メタデータ） (2022-09-15T14:52:31Z) - A Quantum Algorithm for Computing All Diagnoses of a Switching Circuit [73.70667578066775]
ほとんどの人造システム、特にコンピュータは決定論的に機能する。
本稿では、量子物理学が確率法則に従うときの直観的なアプローチである量子情報理論による接続を提供する。
論文 参考訳（メタデータ） (2022-09-08T17:55:30Z) - 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) - PBS-Calculus: A Graphical Language for Coherent Control of Quantum
Computations [77.34726150561087]
本稿では,量子演算のコヒーレント制御を含む量子計算を表現・推論するためにPBS計算を導入する。
我々はこの言語に方程式理論を加え、それが健全で完備であることが証明された。
我々は、制御された置換の実装やループのアンロールのようなアプリケーションを考える。
論文 参考訳（メタデータ） (2020-02-21T16:15:58Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。