A First Step to the Categorical Logic of Quantum Programs

The long-term goal of our research is to develop a powerful quantum logic which is useful in the formal verification of quantum programs and protocols. In this paper we introduce the basic idea of our categorical logic of quantum programs (CLQP): It combines the logic of quantum programming (LQP) an...

Descripción completa

Detalles Bibliográficos
Autores principales: Sun, Xin, He, Feifei
Formato: Online Artículo Texto
Lenguaje:English
Publicado: MDPI 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7516558/
https://www.ncbi.nlm.nih.gov/pubmed/33285919
http://dx.doi.org/10.3390/e22020144
_version_ 1783587029282455552
author Sun, Xin
He, Feifei
author_facet Sun, Xin
He, Feifei
author_sort Sun, Xin
collection PubMed
description The long-term goal of our research is to develop a powerful quantum logic which is useful in the formal verification of quantum programs and protocols. In this paper we introduce the basic idea of our categorical logic of quantum programs (CLQP): It combines the logic of quantum programming (LQP) and categorical quantum mechanics (CQM) such that the advantages of both LQP and CQM are preserved while their disadvantages are overcome. We present the syntax, semantics and proof system of CLQP. As a proof-of-concept, we apply CLQP to verify the correctness of Deutsch’s algorithm and the concealing property of quantum bit commitment.
format Online
Article
Text
id pubmed-7516558
institution National Center for Biotechnology Information
language English
publishDate 2020
publisher MDPI
record_format MEDLINE/PubMed
spelling pubmed-75165582020-11-09 A First Step to the Categorical Logic of Quantum Programs Sun, Xin He, Feifei Entropy (Basel) Article The long-term goal of our research is to develop a powerful quantum logic which is useful in the formal verification of quantum programs and protocols. In this paper we introduce the basic idea of our categorical logic of quantum programs (CLQP): It combines the logic of quantum programming (LQP) and categorical quantum mechanics (CQM) such that the advantages of both LQP and CQM are preserved while their disadvantages are overcome. We present the syntax, semantics and proof system of CLQP. As a proof-of-concept, we apply CLQP to verify the correctness of Deutsch’s algorithm and the concealing property of quantum bit commitment. MDPI 2020-01-24 /pmc/articles/PMC7516558/ /pubmed/33285919 http://dx.doi.org/10.3390/e22020144 Text en © 2020 by the authors. Licensee MDPI, Basel, Switzerland. This article is an open access article distributed under the terms and conditions of the Creative Commons Attribution (CC BY) license (http://creativecommons.org/licenses/by/4.0/).
spellingShingle Article
Sun, Xin
He, Feifei
A First Step to the Categorical Logic of Quantum Programs
title A First Step to the Categorical Logic of Quantum Programs
title_full A First Step to the Categorical Logic of Quantum Programs
title_fullStr A First Step to the Categorical Logic of Quantum Programs
title_full_unstemmed A First Step to the Categorical Logic of Quantum Programs
title_short A First Step to the Categorical Logic of Quantum Programs
title_sort first step to the categorical logic of quantum programs
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7516558/
https://www.ncbi.nlm.nih.gov/pubmed/33285919
http://dx.doi.org/10.3390/e22020144
work_keys_str_mv AT sunxin afirststeptothecategoricallogicofquantumprograms
AT hefeifei afirststeptothecategoricallogicofquantumprograms
AT sunxin firststeptothecategoricallogicofquantumprograms
AT hefeifei firststeptothecategoricallogicofquantumprograms

Ejemplares similares