{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,5]],"date-time":"2026-10-05T20:23:26Z","timestamp":1791231806602,"version":"4.1.0"},"reference-count":78,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,1,16]]},"abstract":"<jats:p>\n            <jats:italic>Quantum programming languages<\/jats:italic>\n            enable developers to implement algorithms for quantum computers that promise computational breakthroughs in classically intractable tasks. Programming quantum computers requires awareness of\n            <jats:italic>entanglement<\/jats:italic>\n            , the phenomenon in which measurement outcomes of qubits are correlated. Entanglement can determine the correctness of algorithms and suitability of programming patterns.\n          <\/jats:p>\n          <jats:p>\n            In this work, we formalize\n            <jats:italic>purity<\/jats:italic>\n            as a central tool for automating reasoning about entanglement in quantum programs. A pure expression is one whose evaluation is unaffected by the measurement outcomes of qubits that it does not own, implying freedom from entanglement with any other expression in the computation.\n          <\/jats:p>\n          <jats:p>We present Twist, the first language that features a type system for sound reasoning about purity. The type system enables the developer to identify pure expressions using type annotations. Twist also features purity assertion operators that state the absence of entanglement in the output of quantum gates. To soundly check these assertions, Twist uses a combination of static analysis and runtime verification.<\/jats:p>\n          <jats:p>We evaluate Twist\u2019s type system and analyses on a benchmark suite of quantum programs in simulation, demonstrating that Twist can express quantum algorithms, catch programming errors in them, and support programs that existing languages disallow, while incurring runtime verification overhead of less than 3.5%.<\/jats:p>","DOI":"10.1145\/3498691","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T17:03:12Z","timestamp":1642006992000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":30,"title":["Twist: sound reasoning for purity and entanglement in Quantum programs"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4918-4467","authenticated-orcid":false,"given":"Charles","family":"Yuan","sequence":"first","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4927-0613","authenticated-orcid":false,"given":"Christopher","family":"McNally","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6928-0456","authenticated-orcid":false,"given":"Michael","family":"Carbin","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Qiskit: An Open-source Framework for Quantum Computing.","author":"Abraham H\u00e9ctor","year":"2019","unstructured":"H\u00e9ctor Abraham . 2019 . Qiskit: An Open-source Framework for Quantum Computing. H\u00e9ctor Abraham. 2019. Qiskit: An Open-source Framework for Quantum Computing."},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.1"},{"key":"e_1_2_2_3_1","volume-title":"Svore","author":"Amy Matthew","year":"2017","unstructured":"Matthew Amy , Martin Roetteler , and Krysta M . Svore . 2017 . Verified Compilation of Space-Efficient Reversible Circuits. In Computer Aided Verification . Matthew Amy, Martin Roetteler, and Krysta M. Svore. 2017. Verified Compilation of Space-Efficient Reversible Circuits. In Computer Aided Verification."},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1080\/09500340.2017.1397221"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371123"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371089"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysicsPhysiqueFizika.1.195"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2014.05.025"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.70.1895"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1038\/nature23474"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386007"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1047659.1040327"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_4"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.87.167902"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.54.1098"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.1801723115"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371131"},{"key":"e_1_2_2_18_1","unstructured":"D. Coppersmith. 1994. An approximate Fourier transform useful in quantum factoring.  D. Coppersmith. 1994. An approximate Fourier transform useful in quantum factoring."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1098\/rspa.1992.0167"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_51"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1371\/journal.pone.0208073"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1088\/1751-8113\/40\/11\/014"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02163027"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1038\/46503"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462177"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-0849-4_10"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/237814.237866"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/780542.780545"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.2307\/1968346"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428201"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2432622.2432625"},{"key":"e_1_2_2_32_1","first-page":"5","article-title":"Two-Message Quantum Interactive Proofs and the Quantum Separability Problem. Quantum Info","volume":"14","author":"Hayden Patrick","year":"2014","unstructured":"Patrick Hayden , Kevin Milner , and Mark M. Wilde . 2014 . Two-Message Quantum Interactive Proofs and the Quantum Separability Problem. Quantum Info . Comput. , 14 , 5 - 6 (2014), April, https:\/\/doi.org\/10.5555\/2638661.2638663 Patrick Hayden, Kevin Milner, and Mark M. Wilde. 2014. Two-Message Quantum Interactive Proofs and the Quantum Separability Problem. Quantum Info. Comput., 14, 5-6 (2014), April, https:\/\/doi.org\/10.5555\/2638661.2638663","journal-title":"Comput."},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2076674.2076675"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434318"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.195.19"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0375-9601(96)00706-2"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3307650.3322213"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290344"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2597917.2597939"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1098\/rspa.2002.1097"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1146\/annurev-physchem-032210-103512"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1070\/RM1997V052N06ABEH002155"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.2172\/366453"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1038\/s41598-020-70446-8"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428218"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/HPCA51647.2021.00025"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-2789(98)00053-0"},{"key":"e_1_2_2_48_1","first-page":"5","article-title":"Constant-Optimized Quantum Circuits for Modular Multiplication and Exponentiation. Quantum Info","volume":"12","author":"Markov Igor L.","year":"2012","unstructured":"Igor L. Markov and Mehdi Saeedi . 2012 . Constant-Optimized Quantum Circuits for Modular Multiplication and Exponentiation. Quantum Info . Comput. , 12 , 5 - 6 (2012), May. Igor L. Markov and Mehdi Saeedi. 2012. Constant-Optimized Quantum Circuits for Modular Multiplication and Exponentiation. Quantum Info. Comput., 12, 5-6 (2012), May.","journal-title":"Comput."},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1117\/12.883332"},{"key":"e_1_2_2_50_1","volume-title":"Chuang","author":"Nielsen Michael A.","year":"2010","unstructured":"Michael A. Nielsen and Isaac L . Chuang . 2010 . Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press . Michael A. Nielsen and Isaac L. Chuang. 2010. Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press."},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454040"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1038\/404130b0"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009894"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.12.015"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69166-2_18"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03745-0_25"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.287.17"},{"key":"e_1_2_2_58_1","volume-title":"Extending Gottesman Types Beyond the Clifford Group. In Workshop on Programming Languages for Quantum Computing.","author":"Rand Robert","year":"2021","unstructured":"Robert Rand , Aarthi Sundaram , Kartik Singhal , and Brad Lackey . 2021 . Extending Gottesman Types Beyond the Clifford Group. In Workshop on Programming Languages for Quantum Computing. Robert Rand, Aarthi Sundaram, Kartik Singhal, and Brad Lackey. 2021. Extending Gottesman Types Beyond the Clifford Group. In Workshop on Programming Languages for Quantum Computing."},{"key":"e_1_2_2_59_1","unstructured":"Robert Rand Aarthi Sundaram Kartik Singhal and Brad Lackey. 2021. Static Analysis of Quantum Programs via Gottesman Types. arxiv:2101.08939.  Robert Rand Aarthi Sundaram Kartik Singhal and Brad Lackey. 2021. Static Analysis of Quantum Programs via Gottesman Types. arxiv:2101.08939."},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-16(1:30)2020"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01449770"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004256"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005238"},{"key":"e_1_2_2_65_1","unstructured":"Yunong Shi Runzhou Tao Xupeng Li Ali Javadi-Abhari Andrew W. Cross Frederic T. Chong and Ronghui Gu. 2020. CertiQ: A Mostly-automated Verification of a Realistic Quantum Compiler. arxiv:1908.08963.  Yunong Shi Runzhou Tao Xupeng Li Ali Javadi-Abhari Andrew W. Cross Frederic T. Chong and Ronghui Gu. 2020. CertiQ: A Mostly-automated Verification of a Realistic Quantum Compiler. arxiv:1908.08963."},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539795293172"},{"key":"e_1_2_2_67_1","unstructured":"Kartik Singhal. 2020. Quantum Hoare Type Theory. arxiv:2012.02154.  Kartik Singhal. 2020. Quantum Hoare Type Theory. arxiv:2012.02154."},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10672-9_11"},{"key":"e_1_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/3183895.3183901"},{"key":"e_1_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454029"},{"key":"e_1_2_2_71_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785779"},{"key":"e_1_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.40.2847"},{"key":"e_1_2_2_73_1","doi-asserted-by":"publisher","DOI":"10.1038\/nature04627"},{"key":"e_1_2_2_74_1","volume-title":"Svore","author":"Wecker Dave","year":"2014","unstructured":"Dave Wecker , Krysta M. Svore , and Krysta M . Svore . 2014 . LIQUi|>: A Software Design Architecture and Domain-Specific Language for Quantum Computing . February. Dave Wecker, Krysta M. Svore, and Krysta M. Svore. 2014. LIQUi|>: A Software Design Architecture and Domain-Specific Language for Quantum Computing. February."},{"key":"e_1_2_2_75_1","doi-asserted-by":"publisher","DOI":"10.1038\/299802a0"},{"key":"e_1_2_2_76_1","volume-title":"Foundations of Quantum Programming","author":"Ying Mingsheng","unstructured":"Mingsheng Ying . 2016. Foundations of Quantum Programming ( 1 st ed.). Morgan Kaufmann Publishers Inc ., San Francisco, CA, USA. isbn:0128023066 Mingsheng Ying. 2016. Foundations of Quantum Programming (1st ed.). Morgan Kaufmann Publishers Inc., San Francisco, CA, USA. isbn:0128023066","edition":"1"},{"key":"e_1_2_2_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454061"},{"key":"e_1_2_2_78_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470673"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498691","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498691","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:28Z","timestamp":1750188628000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498691"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":78,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498691"],"URL":"https:\/\/doi.org\/10.1145\/3498691","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,1,12]]},"assertion":[{"value":"2022-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}