Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

Elsevier eBooks

Foundations of Quantum Programming

Published Jan 1, 2024• 9 citations
Publisher
DOI
10.1016/c2022-0-02250-9

Related papers

Foundations of Quantum Programming

Elsevier eBooks•Jan 1, 2016•93 citations

Foundations of Quantum Programming (Extended Abstract)

Mingsheng Ying

Lecture notes in computer science•Jan 1, 2010•6 citations

Hoare Logic for Quantum Programs

Mingsheng Ying

Hoare logic is a foundation of axiomatic semantics of classical programs and it provides effective proof techniques for reasoning about correctness of classical programs. To offer similar techniques for quantum program verification and to build a logical foundation of programming methodology for quantum computers, we develop a full-fledged Hoare logic for both partial and total correctness of quantum programs. It is proved that this logic is (relatively) complete by exploiting the power of weakest preconditions and weakest liberal preconditions for quantum programs.

arXiv:0906.4586•Jun 25, 2009•9 citations

Quantum programming: From theories to implementations

Mingsheng Ying, Yuan Feng, Runyao Duan +2 more

Chinese Science Bulletin•May 31, 2012•12 citations

Floyd--hoare logic for quantum programs

Mingsheng Ying

Floyd--Hoare logic is a foundation of axiomatic semantics of classical programs, and it provides effective proof techniques for reasoning about correctness of classical programs. To offer similar techniques for quantum program verification and to build a logical foundation of programming methodology for quantum computers, we develop a full-fledged Floyd--Hoare logic for both partial and total correctness of quantum programs. It is proved that this logic is (relatively) complete by exploiting the power of weakest preconditions and weakest liberal preconditions for quantum programs.

ACM Transactions on Programming Languages and Systems•Dec 1, 2011•187 citations

Foundational Design of Multi-Modal Typed Programming Language for Quantum-Classical Hybrid Computing System

Shota Arakaki, Masao Hirokawa

As quantum computing hardware advances toward practical implementation, the design of high-level programming languages for quantum-classical hybrid systems remains a critical challenge. Current quantum programming approaches lack unified abstractions that seamlessly integrate classical and quantum computation. This paper proposes a foundational framework for a high-level quantum-classical hybrid programming language based on multi-modal type theory. Our approach formulates quantum-classical hybrid computation as staged computation, where classical computation generates and executes quantum programs. We adapt type systems and operational semantics from prior research in classical staged computation to this framework. This research provides a theoretical foundation for implementing interpreters and compilers that uniformly handle both classical and quantum computation.

International Conference on Artificial Intelligence, Computer, Data Sciences and Applications (ACDSA)•Feb 5, 2026•0 citations
Hoare logic is a foundation of axiomatic semantics of classical programs and it provides effective proof techniques for reasoning about correctness of classical programs. To offer similar techniques for quantum program verification and to build a logical foundation of programming methodology for quantum computers, we develop a full-fledged Hoare logic for both partial and total correctness of quantum programs. It is proved that this logic is (relatively) complete by exploiting the power of weakest preconditions and weakest liberal preconditions for quantum programs.
Floyd--Hoare logic is a foundation of axiomatic semantics of classical programs, and it provides effective proof techniques for reasoning about correctness of classical programs. To offer similar techniques for quantum program verification and to build a logical foundation of programming methodology for quantum computers, we develop a full-fledged Floyd--Hoare logic for both partial and total correctness of quantum programs. It is proved that this logic is (relatively) complete by exploiting the power of weakest preconditions and weakest liberal preconditions for quantum programs.
As quantum computing hardware advances toward practical implementation, the design of high-level programming languages for quantum-classical hybrid systems remains a critical challenge. Current quantum programming approaches lack unified abstractions that seamlessly integrate classical and quantum computation. This paper proposes a foundational framework for a high-level quantum-classical hybrid programming language based on multi-modal type theory. Our approach formulates quantum-classical hybrid computation as staged computation, where classical computation generates and executes quantum programs. We adapt type systems and operational semantics from prior research in classical staged computation to this framework. This research provides a theoretical foundation for implementing interpreters and compilers that uniformly handle both classical and quantum computation.