{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,29]],"date-time":"2024-07-29T01:10:59Z","timestamp":1722215459903},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2015,8,20]],"date-time":"2015-08-20T00:00:00Z","timestamp":1440028800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Soft Comput"],"published-print":{"date-parts":[[2017,3]]},"DOI":"10.1007\/s00500-015-1802-6","type":"journal-article","created":{"date-parts":[[2015,8,19]],"date-time":"2015-08-19T07:08:58Z","timestamp":1439968138000},"page":"1421-1441","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Deriving the correctness of quantum protocols in the probabilistic logic for quantum programs"],"prefix":"10.1007","volume":"21","author":[{"given":"Jort Martinus","family":"Bergfeld","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joshua","family":"Sack","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,8,20]]},"reference":[{"key":"1802_CR1","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1016\/B978-0-444-52869-8.50010-4","volume-title":"Handbook of quantum logic and quantum structures","author":"S Abramsky","year":"2009","unstructured":"Abramsky S, Coecke B (2009) Categorical quantum mechanics. In: Lehmann D, Engesser K, Gabbay DM (eds) Handbook of quantum logic and quantum structures. Elsevier, Amsterdam, pp 261\u2013323"},{"issue":"12","key":"1802_CR2","doi-asserted-by":"crossref","first-page":"2267","DOI":"10.1007\/s10773-005-8022-2","volume":"44","author":"A Baltag","year":"2005","unstructured":"Baltag A, Smets S (2005) Complete axiomatizations for quantum actions. Int J Theor Phys 44(12):2267\u20132282","journal-title":"Int J Theor Phys"},{"issue":"3","key":"1802_CR3","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1017\/S0960129506005299","volume":"16","author":"A Baltag","year":"2006","unstructured":"Baltag A, Smets S (2006) LQP: the dynamic logic of quantum information. Math Struct Comput Sci 16(3):491\u2013525","journal-title":"Math Struct Comput Sci"},{"key":"1802_CR4","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1007\/978-3-642-39992-3_9","volume-title":"Logic, language, information, and computation, lecture notes in computer science","author":"A Baltag","year":"2013","unstructured":"Baltag A, Bergfeld J, Kishida K, Sack J, Smets S, Zhong S (2013) Quantum probabilistic dyadic second-order logic. In: Libkin L, Kohlenbach U, de Queiroz R (eds) Logic, language, information, and computation, lecture notes in computer science, vol 8071. Springer, Berlin, Heidelberg, pp 64\u201380"},{"issue":"10","key":"1802_CR5","doi-asserted-by":"crossref","first-page":"3628","DOI":"10.1007\/s10773-013-1987-3","volume":"53","author":"A Baltag","year":"2014","unstructured":"Baltag A, Bergfeld J, Kishida K, Sack J, Smets S, Zhong S (2014) PLQP & company: decidable logics for quantum algorithms. Int J Theor Phys 53(10):3628\u20133647","journal-title":"Int J Theor Phys"},{"key":"1802_CR6","unstructured":"Bennett CH, Brassard G (1984) Quantum cryptography: public key distribution and coin tossing. In: Proceedings of IEEE international conference on computers, systems and signal processing, pp 175\u2013179"},{"key":"1802_CR7","doi-asserted-by":"crossref","unstructured":"Bennett CH, Brassard G (2014) Quantum cryptography: public key distribution and coin tossing. In: Theoretical computer science 560, Part 1, theoretical aspects of quantum cryptography\u2014celebrating 30 years of BB84, pp 7\u201311","DOI":"10.1016\/j.tcs.2014.05.025"},{"key":"1802_CR8","doi-asserted-by":"publisher","unstructured":"Bergfeld JM, Kishida K, Sack J, Zhong S (2015) Duality for the logic of quantum actions. Stud Log 103(4):781\u2013805. doi: 10.1007\/s11225-014-9592-x","DOI":"10.1007\/s11225-014-9592-x"},{"key":"1802_CR9","doi-asserted-by":"crossref","first-page":"823","DOI":"10.2307\/1968621","volume":"37","author":"G Birkhoff","year":"1936","unstructured":"Birkhoff G, von Neumann J (1936) The logic of quantum mechanics. Ann Math 37:823\u2013843","journal-title":"Ann Math"},{"key":"1802_CR10","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1007\/978-94-017-0460-1_2","volume-title":"Handbook of philosophical logic","author":"ML Dalla Chiara","year":"2002","unstructured":"Dalla Chiara ML, Giuntini R (2002) Quantum logics. In: Gabbay D, Guenthner F (eds) Handbook of philosophical logic. Kluwer Academic Publishers, Dordrecht, pp 129\u2013228"},{"key":"1802_CR11","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-0526-4","volume-title":"Reasoning in quantum theory: sharp and unsharp quantum logics, trends in logic","author":"ML Dalla Chiara","year":"2004","unstructured":"Dalla Chiara ML, Giuntini R, Greechie R (2004) Reasoning in quantum theory: sharp and unsharp quantum logics, trends in logic, vol 22. Kluwer Academic Press, Dordrecht"},{"key":"1802_CR12","doi-asserted-by":"crossref","unstructured":"D\u2019Hondt E, Panangaden P (2006a) The computational power of the W and GHZ states. Quantum Inf Comput 6(2):173\u2013183","DOI":"10.26421\/QIC6.2-3"},{"key":"1802_CR13","doi-asserted-by":"crossref","unstructured":"D\u2019Hondt E, Panangaden P (2006b) Quantum weakest preconditions. Math Struct Comput Sci 16:429\u2013451 6","DOI":"10.1017\/S0960129506005251"},{"issue":"3","key":"1802_CR14","doi-asserted-by":"crossref","first-page":"443","DOI":"10.1007\/s10992-013-9273-7","volume":"42","author":"JM Dunn","year":"2013","unstructured":"Dunn JM, Moss LS, Wang Z (2013) Editors\u2019 introduction: the third life of quantum logic: quantum logic inspired by quantum computing. J Philos Log 42(3):443\u2013459","journal-title":"J Philos Log"},{"issue":"2","key":"1802_CR15","doi-asserted-by":"crossref","first-page":"340","DOI":"10.1145\/174652.174658","volume":"41","author":"R Fagin","year":"1994","unstructured":"Fagin R, Halpern JY (1994) Reasoning about knowledge and probability. J ACM 41(2):340\u2013367","journal-title":"J ACM"},{"issue":"1","key":"1802_CR16","doi-asserted-by":"crossref","first-page":"78","DOI":"10.1016\/0890-5401(90)90060-U","volume":"87","author":"R Fagin","year":"1990","unstructured":"Fagin R, Halpern JY, Megiddo N (1990) A logic for reasoning about probabilities. Inf Comput 87(1):78\u2013128","journal-title":"Inf Comput"},{"issue":"7","key":"1802_CR17","doi-asserted-by":"crossref","first-page":"1181","DOI":"10.1016\/j.jcss.2013.04.002","volume":"79","author":"Y Feng","year":"2013","unstructured":"Feng Y, Nengkun Y, Ying M (2013) Model checking quantum Markov chains. J Comput Syst Sci 79(7):1181\u20131198","journal-title":"J Comput Syst Sci"},{"issue":"2","key":"1802_CR18","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"MJ Fischer","year":"1979","unstructured":"Fischer MJ, Ladner RE (1979) Propositional dynamic logic of regular programs. J Comput Syst Sci 18(2):194\u2013211","journal-title":"J Comput Syst Sci"},{"key":"1802_CR19","doi-asserted-by":"crossref","unstructured":"Gay SJ, Nagarajan R, Papanikolaou N (2008) QMC: a model checker for quantum systems. In: Proceedings of the 20th international conference on computer aided verification, CAV \u201908. Springer, Berlin, Heidelberg, pp 543\u2013547","DOI":"10.1007\/978-3-540-70545-1_51"},{"issue":"1\u20132","key":"1802_CR20","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1007\/BF00652069","volume":"3","author":"RI Goldblatt","year":"1974","unstructured":"Goldblatt RI (1974) Semantic analysis of orthologic. J Philos Log 3(1\u20132):19\u201335","journal-title":"J Philos Log"},{"key":"1802_CR21","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic logic","author":"D Harel","year":"2000","unstructured":"Harel D, Tiuryn J, Kozen D (2000) Dynamic logic. MIT Press, Cambridge"},{"issue":"10","key":"1802_CR22","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"TCAR Hoare","year":"1969","unstructured":"Hoare TCAR (1969) An axiomatic basis for computer programming. Commun ACM 12(10):576\u2013580","journal-title":"Commun ACM"},{"key":"1802_CR23","unstructured":"Hodkinson I, Reynolds M (2007) Temporal logic. In: Blackburn P, Van Benthem J, Wolter F (eds) Handbook of modal logic, studies in logic and practical reasoning, chapter 11, vol 3. Elsevier, pp 655\u2013720"},{"issue":"5","key":"1802_CR24","doi-asserted-by":"crossref","first-page":"771","DOI":"10.1016\/j.ic.2006.02.001","volume":"204","author":"P Mateus","year":"2006","unstructured":"Mateus P, Sernadas A (2006) Weakly complete axiomatization of exogenous quantum propositional logic. Inf Comput 204(5):771\u2013794","journal-title":"Inf Comput"},{"key":"1802_CR25","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/B978-0-444-52869-8.50009-8","volume-title":"Handbook of quantum logic and quantum structures","author":"H Nishimura","year":"2009","unstructured":"Nishimura H (2009) Gentzen methods in quantum logic. In: Lehmann D, Engesser K, Gabbay DM (eds) Handbook of quantum logic and quantum structures. Elsevier, Amsterdam, pp 227\u2013260"},{"key":"1802_CR26","unstructured":"Selinger P (2007) Dagger compact closed categories and completely positive maps: (extended abstract). In: Electronic notes in theoretical computer science. Proceedings of the 3rd international workshop on quantum programming languages (QPL 2005), vol 170, pp 139\u2013163"},{"key":"1802_CR27","doi-asserted-by":"crossref","unstructured":"Selinger P (2011) Finite dimensional Hilbert spaces are complete for dagger compact closed categories (extended abstract). In: Electronic notes in theoretical computer science. Proceedings of the joint 5th international workshop on quantum physics and logic and 4th workshop on developments in computational models (QPL\/DCM 2008), vol 270(1), pp 113\u2013119","DOI":"10.1016\/j.entcs.2011.01.010"},{"key":"1802_CR28","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-8(3:6)2012","volume":"8","author":"P Selinger","year":"2012","unstructured":"Selinger P (2012) Finite dimensional Hilbert spaces are complete for dagger compact closed categories. Log Methods Comput Sci 8:1\u201312","journal-title":"Log Methods Comput Sci"},{"key":"1802_CR29","unstructured":"Smets S, Baltag A (2006) Logics for quantum information flow. In: Presented at the 18-th European Summer School of Logic, Language and Information. http:\/\/www.vub.ac.be\/CLWF\/SS\/slides.html . Accessed 14 Dec 2014"},{"key":"1802_CR30","doi-asserted-by":"crossref","unstructured":"Tani S, Kobayashi H, Matsumoto K (2012) Exact quantum algorithms for the leader election problem. ACM Trans Comput Theory 4(1):1:1\u20131:24","DOI":"10.1145\/2141938.2141939"},{"issue":"9","key":"1802_CR31","doi-asserted-by":"crossref","first-page":"1679","DOI":"10.1016\/j.scico.2013.03.016","volume":"78","author":"M Ying","year":"2013","unstructured":"Ying M, Nengkun Y, Feng Y, Duan R (2013) Verification of quantum programs. Sci Comput Program 78(9):1679\u20131700","journal-title":"Sci Comput Program"}],"container-title":["Soft Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00500-015-1802-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00500-015-1802-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00500-015-1802-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00500-015-1802-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,20]],"date-time":"2022-05-20T16:38:59Z","timestamp":1653064739000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00500-015-1802-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,8,20]]},"references-count":31,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2017,3]]}},"alternative-id":["1802"],"URL":"https:\/\/doi.org\/10.1007\/s00500-015-1802-6","relation":{},"ISSN":["1432-7643","1433-7479"],"issn-type":[{"value":"1432-7643","type":"print"},{"value":"1433-7479","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,8,20]]}}}