constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
quantum algorithms:
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
QPMC
is a software verification-tool for quantum programming languages (a “Quantum Protocol Model Checker”).
Introducing QPMC
:
Yuan Feng, Ernst Moritz Hahn, Andrea Turrini, Lijun Zhang, QPMC
: A Model Checker for Quantum Programs and Protocols, in Formal Methods. FM 2015, Lecture Notes in Computer Science 9109, Springer (2015) [doi:10.1007/978-3-319-19249-9_17]
“In practice, however, security analysis of quantum cryptographic protocols is notoriously difficult; for example, the manual proof of BB84 in [15] contains about 50 pages. It is hard to imagine such an analysis being carried out for more sophisticated quantum protocols. Thus, techniques for automated or semi-automated verification of these protocols will be indispensable.”
Background and review:
Mingsheng Ying, Yuan Feng, Model Checking Quantum Systems — A Survey [arXiv:1807.09466]
“But to check whether a quantum system satisfies a certain property at a time point, one has to perform a quantum. measurement on the system, which can change the state of the system. This makes studies of the long-term behaviours of quantum systems much harder than that of classical system.”
“The state spaces of the classical systems that model-checking algorithms can be applied to are usually finite or countably infinite. However, the state spaces of quantum systems are inherently continuous even when they are finite-dimensional. In order to develop algorithms for model-checking quantum systems, we have to exploit some deep mathematical properties of the systems so that it suffices to examine only a finite number of (or at most countably infinitely many) representative elements, e.g. those in an orthonormal basis, of their state spaces.”
On verification of Quipper-programs with QPMC:
Created on March 3, 2023 at 07:27:26. See the history of this page for a list of all contributions to it.