{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T07:09:07Z","timestamp":1648883347791},"reference-count":24,"publisher":"Open Publishing Association","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electron. Proc. Theor. Comput. Sci.","EPTCS"],"DOI":"10.4204\/eptcs.340.15","type":"journal-article","created":{"date-parts":[[2021,9,6]],"date-time":"2021-09-06T16:58:12Z","timestamp":1630947492000},"page":"291-302","source":"Crossref","is-referenced-by-count":0,"title":["Quantum Hoare Type Theory: Extended Abstract"],"prefix":"10.4204","volume":"340","author":[{"given":"Kartik","family":"Singhal","sequence":"first","affiliation":[{"name":"University of Chicago"}]},{"given":"John","family":"Reppy","sequence":"additional","affiliation":[{"name":"University of Chicago"}]}],"member":"2720","published-online":{"date-parts":[[2021,9,6]]},"reference":[{"key":"qio","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1017\/CBO9781139193313.006","article-title":"The Quantum IO Monad","volume-title":"Semantic Techniques in Quantum Computation","author":"Altenkirch","year":"2009"},{"key":"amy18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.4204\/EPTCS.287.1","article-title":"Towards Large-scale Functional Verification of Universal Quantum Circuits","volume-title":"Proc. QPL '18","author":"Amy","year":"2018"},{"key":"dijkstra1976","volume-title":"A Discipline of Programming","author":"Dijkstra","year":"1976"},{"issue":"3","key":"dhondt2006","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1017\/S0960129506005251","article-title":"Quantum Weakest Preconditions","volume":"16","author":"D'hondt","year":"2006","journal-title":"Math. Struct. Comput. Sci."},{"key":"fu2020linear","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394765","article-title":"Linear Dependent Type Theory for Quantum Programming Languages: Extended Abstract","volume-title":"Proc. LICS '20","author":"Fu","year":"2020"},{"key":"fqc06","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/j.entcs.2008.04.018","article-title":"From Reversible to Irreversible Computations","volume":"210","author":"Green","year":"2008","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"asg2010","volume-title":"Towards a formally verified functional quantum programming language","author":"Green","year":"2010"},{"key":"huang2018","doi-asserted-by":"publisher","DOI":"10.4230\/OASIcs.PLATEAU.2018.4","article-title":"QDB: From Quantum Algorithms Towards Correct Quantum Programs","volume-title":"9th Workshop on Evaluation and Usability of Programming Languages and Tools (PLATEAU '18)","author":"Huang","year":"2018"},{"key":"huang2019","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1145\/3307650.3322213","article-title":"Statistical Assertions for Validating Patterns and Finding Bugs in Quantum Programs","volume-title":"Proc. ISCA '19","author":"Huang","year":"2019"},{"issue":"10","key":"hoare1969","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","article-title":"An Axiomatic Basis for Computer Programming","volume":"12","author":"Hoare","year":"1969","journal-title":"Commun. ACM"},{"key":"JorrandPerdrix2009","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1017\/CBO9781139193313.007","article-title":"Abstract Interpretation Techniques for Quantum Computation","volume-title":"Semantic Techniques in Quantum Computation","author":"Jorrand","year":"2009"},{"key":"nielsen2010","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511976667","volume-title":"Quantum Computation and Quantum Information","author":"Nielsen","year":"2010"},{"issue":"56","key":"htt-jfp","doi-asserted-by":"publisher","first-page":"865","DOI":"10.1017\/S0956796808006953","article-title":"Hoare Type Theory, Polymorphism and Separation","volume":"18","author":"Nanevski","year":"2008","journal-title":"J. Funct. Program."},{"key":"ynot2008","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1145\/1411204.1411237","article-title":"Ynot: Dependent Types for Imperative Programs","volume-title":"Proc. ICFP 08","author":"Nanevski","year":"2008"},{"key":"Paykin2017","doi-asserted-by":"publisher","first-page":"846","DOI":"10.1145\/3009837.3009894","article-title":"QWIRE: A Core Language for Quantum Circuits","volume-title":"Proc. POPL '17","author":"Paykin","year":"2017"},{"key":"rand2018","volume-title":"Formally Verified Quantum Programming","author":"Rand","year":"2018"},{"key":"reynolds2002","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1109\/LICS.2002.1029817","article-title":"Separation Logic: A Logic for Shared Mutable Data Structures","volume-title":"Proc. LICS '02","author":"Reynolds","year":"2002"},{"key":"ross2015","volume-title":"Algebraic and Logical Methods in Quantum Computation","author":"Ross","year":"2015"},{"key":"rand2017","doi-asserted-by":"publisher","first-page":"119","DOI":"10.4204\/EPTCS.266.8","article-title":"QWIRE Practice: Formal Verification of Quantum Circuits in Coq","volume-title":"Proc. QPL '17","author":"Rand","year":"2018"},{"key":"rios2017","doi-asserted-by":"publisher","first-page":"164","DOI":"10.4204\/EPTCS.266.11","article-title":"A Categorical Model for a Quantum Circuit Description Language (Extended Abstract)","volume-title":"Proc. QPL '17","author":"Rios","year":"2017"},{"key":"rssl20","series-title":"this volume of EPTCS","article-title":"Gottesman Types for Quantum Programs","volume-title":"Proc. QPL '20","author":"Rand","year":"2020"},{"key":"unruh2019","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/LICS.2019.8785779","article-title":"Quantum Hoare Logic with Ghost Variables","volume-title":"Proc. LICS '19","author":"Unruh","year":"2019"},{"issue":"3","key":"so-arrows","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1017\/S0960129506005287","article-title":"Structuring Quantum Effects: Superoperators as Arrows","volume":"16","author":"Vizzotto","year":"2006","journal-title":"Math. Struct. Comput. Sci."},{"issue":"6","key":"ying2012","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708","article-title":"Floyd\u2013Hoare Logic for Quantum Programs","volume":"33","author":"Ying","year":"2012","journal-title":"ACM Trans. Program. Lang. Syst."}],"container-title":["Electronic Proceedings in Theoretical Computer Science"],"original-title":[],"language":"en","deposited":{"date-parts":[[2021,9,8]],"date-time":"2021-09-08T03:10:55Z","timestamp":1631070655000},"score":1,"resource":{"primary":{"URL":"http:\/\/arxiv.org\/abs\/2109.02198v1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,9,6]]},"references-count":24,"URL":"https:\/\/doi.org\/10.4204\/eptcs.340.15","relation":{},"ISSN":["2075-2180"],"issn-type":[{"value":"2075-2180","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,9,6]]}}}