@inproceedings{Peng2022,
  title         = {Algebraic Reasoning of Quantum Programs via Non-Idempotent Kleene Algebra},
  author        = {Peng, Yuxiang and Ying, Mingsheng and Wu, Xiaodi},
  year          = {2022},
  month         = jun,
  booktitle     = {Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation},
  publisher     = acm,
  address       = {New York, NY, USA},
  series        = {{{PLDI}} '22},
  pages         = {657--670},
  numpages      = {14},
  doi           = {10.1145/3519939.3523713},
  archiveprefix = {arXiv},
  eprint        = {2110.07018},
  abstract      = {We investigate the algebraic reasoning of quantum programs inspired by the success of classical program analysis based on Kleene algebra. One prominent example of such is the famous Kleene Algebra with Tests (KAT), which has furnished both theoretical insights and practical tools. The succinctness of algebraic reasoning would be especially desirable for scalable analysis of quantum programs, given the involvement of exponential-size matrices in most of the existing methods. A few key features of KAT including the idempotent law and the nice properties of classical tests, however, fail to hold in the context of quantum programs due to their unique quantum features, especially in branching. We propose the Non-idempotent Kleena Algebra (NKA) as a natural alternative, and identify complete and sound semantic models for NKA as well as their quantum interpretations. In light of applications of KAT, we demonstrate algebraic proofs in NKA of quantum compiler optimization and the normal form of quantum \textbf{while}-programs. Moreover, we extend NKA with Tests (i.e., NKAT), where tests model quantum predicates following effect algebra, and illustrate how to encode propositional quantum Hoare logic as NKAT theorems.},
  keywords      = {non-idempotent kleene algebra, compiler optimization, normal form theorem, quantum hoare logic},
  webnote       = {See arXiv for extended version.},
  bibsource     = qplbib
}

{"_id":"ziaKhrakTcprgcyhB","bibbaseid":"peng-ying-wu-algebraicreasoningofquantumprogramsvianonidempotentkleenealgebra-2022","author_short":["Peng, Y.","Ying, M.","Wu, X."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","title":"Algebraic Reasoning of Quantum Programs via Non-Idempotent Kleene Algebra","author":[{"propositions":[],"lastnames":["Peng"],"firstnames":["Yuxiang"],"suffixes":[]},{"propositions":[],"lastnames":["Ying"],"firstnames":["Mingsheng"],"suffixes":[]},{"propositions":[],"lastnames":["Wu"],"firstnames":["Xiaodi"],"suffixes":[]}],"year":"2022","month":"June","booktitle":"Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation","publisher":"Association for Computing Machinery","address":"New York, NY, USA","series":"PLDI '22","pages":"657–670","numpages":"14","doi":"10.1145/3519939.3523713","archiveprefix":"arXiv","eprint":"2110.07018","abstract":"We investigate the algebraic reasoning of quantum programs inspired by the success of classical program analysis based on Kleene algebra. One prominent example of such is the famous Kleene Algebra with Tests (KAT), which has furnished both theoretical insights and practical tools. The succinctness of algebraic reasoning would be especially desirable for scalable analysis of quantum programs, given the involvement of exponential-size matrices in most of the existing methods. A few key features of KAT including the idempotent law and the nice properties of classical tests, however, fail to hold in the context of quantum programs due to their unique quantum features, especially in branching. We propose the Non-idempotent Kleena Algebra (NKA) as a natural alternative, and identify complete and sound semantic models for NKA as well as their quantum interpretations. In light of applications of KAT, we demonstrate algebraic proofs in NKA of quantum compiler optimization and the normal form of quantum \\textbfwhile-programs. Moreover, we extend NKA with Tests (i.e., NKAT), where tests model quantum predicates following effect algebra, and illustrate how to encode propositional quantum Hoare logic as NKAT theorems.","keywords":"non-idempotent kleene algebra, compiler optimization, normal form theorem, quantum hoare logic","webnote":"See arXiv for extended version.","bibsource":"Quantum Programming Languages & Verification Bibliography, https://git.io/qpl-bib","bibtex":"@inproceedings{Peng2022,\n title = {Algebraic Reasoning of Quantum Programs via Non-Idempotent Kleene Algebra},\n author = {Peng, Yuxiang and Ying, Mingsheng and Wu, Xiaodi},\n year = {2022},\n month = jun,\n booktitle = {Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation},\n publisher = acm,\n address = {New York, NY, USA},\n series = {{{PLDI}} '22},\n pages = {657--670},\n numpages = {14},\n doi = {10.1145/3519939.3523713},\n archiveprefix = {arXiv},\n eprint = {2110.07018},\n abstract = {We investigate the algebraic reasoning of quantum programs inspired by the success of classical program analysis based on Kleene algebra. One prominent example of such is the famous Kleene Algebra with Tests (KAT), which has furnished both theoretical insights and practical tools. The succinctness of algebraic reasoning would be especially desirable for scalable analysis of quantum programs, given the involvement of exponential-size matrices in most of the existing methods. A few key features of KAT including the idempotent law and the nice properties of classical tests, however, fail to hold in the context of quantum programs due to their unique quantum features, especially in branching. We propose the Non-idempotent Kleena Algebra (NKA) as a natural alternative, and identify complete and sound semantic models for NKA as well as their quantum interpretations. In light of applications of KAT, we demonstrate algebraic proofs in NKA of quantum compiler optimization and the normal form of quantum \\textbf{while}-programs. Moreover, we extend NKA with Tests (i.e., NKAT), where tests model quantum predicates following effect algebra, and illustrate how to encode propositional quantum Hoare logic as NKAT theorems.},\n keywords = {non-idempotent kleene algebra, compiler optimization, normal form theorem, quantum hoare logic},\n webnote = {See arXiv for extended version.},\n bibsource = qplbib\n}\n\n","author_short":["Peng, Y.","Ying, M.","Wu, X."],"key":"Peng2022","id":"Peng2022","bibbaseid":"peng-ying-wu-algebraicreasoningofquantumprogramsvianonidempotentkleenealgebra-2022","role":"author","urls":{},"keyword":["non-idempotent kleene algebra","compiler optimization","normal form theorem","quantum hoare logic"],"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"https://raw.githubusercontent.com/QuantumPL/bib/main/bbt.bib","dataSources":["JG9W34HAXfSxsC6ML"],"keywords":["non-idempotent kleene algebra","compiler optimization","normal form theorem","quantum hoare logic"],"search_terms":["algebraic","reasoning","quantum","programs","via","non","idempotent","kleene","algebra","peng","ying","wu"],"title":"Algebraic Reasoning of Quantum Programs via Non-Idempotent Kleene Algebra","year":2022}