論文の概要: Quantum Hoare Type Theory: Extended Abstract

• arxiv url: http://arxiv.org/abs/2109.02198v1
• Date: Mon, 6 Sep 2021 01:02:20 GMT
• ステータス: 処理完了
• システム内更新日: 2023-03-16 01:07:20.387630
• Title: Quantum Hoare Type Theory: Extended Abstract
• Title（参考訳）: 量子ホーア型理論:拡張抽象
• Authors: Kartik Singhal (University of Chicago), John Reppy (University of Chicago)
• Abstract要約: 量子コンピューティングでは、フォーマルな検証と音質の静的型システムによって、いくつかのバグが導入されるのを防ぐ。 プログラム仕様として機能する事前条件と後条件をインデックス化してQuantum IO Monadを拡張することで、Quantum Hoare Typesを提案する。 QHTTは、量子プログラムのプログラミング、特定、推論のための統一されたシステムになる可能性を持っている。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: As quantum computers become real, it is high time we come up with effective techniques that help programmers write correct quantum programs. In classical computing, formal verification and sound static type systems prevent several classes of bugs from being introduced. There is a need for similar techniques in the quantum regime. Inspired by Hoare Type Theory in the classical paradigm, we propose Quantum Hoare Types by extending the Quantum IO Monad by indexing it with pre- and post-conditions that serve as program specifications. In this paper, we introduce Quantum Hoare Type Theory (QHTT), present its syntax and typing rules, and demonstrate its effectiveness with the help of examples. QHTT has the potential to be a unified system for programming, specifying, and reasoning about quantum programs. This is a work in progress.
• Abstract（参考訳）: 量子コンピュータが現実になるにつれて、プログラマが正しい量子プログラムを書くのに役立つ効果的なテクニックが思い浮かびます。 古典コンピューティングでは、形式的検証と健全な静的型システムにより、いくつかのバグのクラスが導入されるのを防ぐ。 量子状態には同様の技術が必要である。 古典パラダイムにおけるhoare型理論に着想を得て,量子ioモナドをプログラム仕様として機能するプリ条件とポスト条件でインデックス化することにより,量子hoare型を提案する。 本稿では,QHTT(Quantum Hoare Type Theory)を紹介し,その構文とタイピング規則を示し,実例を用いてその効果を実証する。 QHTTは、量子プログラムのプログラミング、特定、推論のための統一されたシステムになる可能性がある。 これは進行中の作業です。

関連論文リスト

• Quantum types: going beyond qubits and quantum gates [0.0]
  この記事では、高レベルの抽象化の必要性を概説し、Rhymeという開発者フレンドリーなプログラミング言語でそれらをいくつか提案する。 新しい量子型は、ビット、整数、フロート、文字、配列、文字列を含む古典型の拡張である。
  論文  参考訳（メタデータ） (2024-01-26T18:54:35Z)
• QbC: Quantum Correctness by Construction [4.572433350229651]
  提案するQuantum Correctness by Construction (QbC) は,その仕様から量子プログラムを構築するための手法である。 プリコンディションとポストコンディションを使用してプログラム特性を規定し、その仕様から量子状態におけるプログラム構築のための音質および完全改善ルールを提案する。 このアプローチは、プログラムの詳細を導出する方法を自然に提案し、その過程で重要な設計上の選択を強調します。
  論文  参考訳（メタデータ） (2023-07-28T16:00:57Z)
• Quantum data learning for quantum simulations in high-energy physics [55.41644538483948]
  本研究では,高エネルギー物理における量子データ学習の実践的問題への適用性について検討する。 我々は、量子畳み込みニューラルネットワークに基づくアンサッツを用いて、基底状態の量子位相を認識できることを数値的に示す。 これらのベンチマークで示された非自明な学習特性の観察は、高エネルギー物理学における量子データ学習アーキテクチャのさらなる探求の動機となる。
  論文  参考訳（メタデータ） (2023-06-29T18:00:01Z)
• Simple Tests of Quantumness Also Certify Qubits [69.96668065491183]
  量子性の検定は、古典的検証者が証明者が古典的でないことを(のみ)証明できるプロトコルである。 我々は、あるテンプレートに従う量子性のテストを行い、(Kalai et al., 2022)のような最近の提案を捉えた。 すなわち、同じプロトコルは、証明可能なランダム性や古典的な量子計算のデリゲートといったアプリケーションの中心にあるビルディングブロックであるqubitの認定に使用できる。
  論文  参考訳（メタデータ） (2023-03-02T14:18:17Z)
• Quantum Machine Learning: from physics to software engineering [58.720142291102135]
  古典的な機械学習アプローチが量子コンピュータの設備改善にどのように役立つかを示す。 量子アルゴリズムと量子コンピュータは、古典的な機械学習タスクを解くのにどのように役立つかについて議論する。
  論文  参考訳（メタデータ） (2023-01-04T23:37:45Z)
• Qafny: A Quantum-Program Verifier [39.47005122712576]
  本稿では,量子プログラムの自動検証システムであるQafnyを紹介する。 Qafnyの核心は、量子演算を古典的な配列演算に変換する型誘導量子証明システムである。 我々はQafnyが量子ウォークアルゴリズム、Groverのアルゴリズム、Shorのアルゴリズムを含む重要な量子アルゴリズムを効率的に検証する方法を示す。
  論文  参考訳（メタデータ） (2022-11-11T18:50:52Z)
• LQP: The Dynamic Logic of Quantum Information [77.34726150561087]
  本稿では,複合量子システムにおける情報フローの推論のための動的論理形式について紹介する。 本稿では,この論理の文法,関係意味論,音響証明システムについて述べる。 アプリケーションとしては,テレポーテーションプロトコルと標準量子秘密共有プロトコルに対して,正式な正当性を与えるために,我々のシステムを利用する。
  論文  参考訳（メタデータ） (2021-10-04T12:20:23Z)
• Imaginary Time Propagation on a Quantum Chip [50.591267188664666]
  想像時間における進化は、量子多体系の基底状態を見つけるための顕著な技術である。 本稿では,量子コンピュータ上での仮想時間伝搬を実現するアルゴリズムを提案する。
  論文  参考訳（メタデータ） (2021-02-24T12:48:00Z)
• Quantum Hoare Type Theory [0.0]
  量子ホア型理論(Quantum Hoare Type Theory, QHTT)は、古典計算におけるホア型理論に触発された理論である。 QHTTは、量子状態の変更に関する正確な仕様を提供する。
  論文  参考訳（メタデータ） (2020-12-03T18:41:08Z)
• Compiling quantamorphisms for the IBM Q Experience [0.0]
  本稿では,古典的プログラム代数の法則を量子プログラミングに拡張するために貢献する。 IBM Q Experienceで利用可能な量子デバイスにデプロイされるように、正しく構成された量子回路を構築することを目的としている。
  論文  参考訳（メタデータ） (2020-10-21T13:32:24Z)
• Quantum Gram-Schmidt Processes and Their Application to Efficient State Read-out for Quantum Algorithms [87.04438831673063]
  本稿では、生成した状態の古典的ベクトル形式を生成する効率的な読み出しプロトコルを提案する。 我々のプロトコルは、出力状態が入力行列の行空間にある場合に適合する。 我々の技術ツールの1つは、Gram-Schmidt正則手順を実行するための効率的な量子アルゴリズムである。
  論文  参考訳（メタデータ） (2020-04-14T11:05:26Z)

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

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