{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,29]],"date-time":"2026-05-29T14:38:56Z","timestamp":1780065536033,"version":"3.54.0"},"publisher-location":"New York, NY, USA","reference-count":33,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,7,8]],"date-time":"2020-07-08T00:00:00Z","timestamp":1594166400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"AFOSR","award":["FA9550-15-1-0331"],"award-info":[{"award-number":["FA9550-15-1-0331"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,7,8]]},"DOI":"10.1145\/3373718.3394765","type":"proceedings-article","created":{"date-parts":[[2020,5,26]],"date-time":"2020-05-26T00:23:18Z","timestamp":1590452598000},"page":"440-453","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":20,"title":["Linear Dependent Type Theory for Quantum Programming Languages"],"prefix":"10.1145","author":[{"given":"Peng","family":"Fu","sequence":"first","affiliation":[{"name":"Dalhousie University, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kohei","family":"Kishida","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, U.S.A."}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peter","family":"Selinger","sequence":"additional","affiliation":[{"name":"Dalhousie University, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2020,7,8]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209189"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78499-9_26"},{"key":"e_1_3_2_1_4_1","volume-title":"International Workshop on Computer Science Logic. Springer, 121--135","author":"Benton P. Nick","year":"1994","unstructured":"P. Nick Benton . 1994 . A mixed linear and non-linear logic: Proofs, terms and models . In International Workshop on Computer Science Logic. Springer, 121--135 . P. Nick Benton. 1994. A mixed linear and non-linear logic: Proofs, terms and models. In International Workshop on Computer Science Logic. Springer, 121--135."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158093"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/788018.788831"},{"key":"e_1_3_2_1_7_1","volume-title":"Proceedings of the 12th International Conference on Reversible Computation. Springer. To appear.","author":"Fu Peng","year":"2020","unstructured":"Peng Fu , Kohei Kishida , Neil J. Ross , and Peter Selinger . 2020 . A tutorial introduction to quantum circuit programming in dependently typed Proto-Quipper . In Proceedings of the 12th International Conference on Reversible Computation. Springer. To appear. Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger. 2020. A tutorial introduction to quantum circuit programming in dependently typed Proto-Quipper. In Proceedings of the 12th International Conference on Reversible Computation. Springer. To appear."},{"key":"e_1_3_2_1_8_1","unstructured":"Peng Fu Kohei Kishida and Peter Selinger. 2020. Linear dependent type theory for quantum programming languages. (2020). Available from arXiv:2004.13472.  Peng Fu Kohei Kishida and Peter Selinger. 2020. Linear dependent type theory for quantum programming languages. (2020). Available from arXiv:2004.13472."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429113"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90386-T"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38986-3_10"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462177"},{"key":"e_1_3_2_1_14_1","volume-title":"European Symposium on Programming. Springer, 302--316","author":"Barry Jay C.","year":"1994","unstructured":"C. Barry Jay and J. Robin B. Cockett . 1994 . Shapely types and shape polymorphism . In European Symposium on Programming. Springer, 302--316 . C. Barry Jay and J. Robin B. Cockett. 1994. Shapely types and shape polymorphism. In European Symposium on Programming. Springer, 302--316."},{"key":"e_1_3_2_1_15_1","volume-title":"Haskell 98 language and libraries: the revised report","author":"Jones Simon Peyton","unstructured":"Simon Peyton Jones . 2003. Haskell 98 language and libraries: the revised report . Cambridge University Press . Simon Peyton Jones. 2003. Haskell 98 language and libraries: the revised report. Cambridge University Press."},{"key":"e_1_3_2_1_16_1","volume-title":"Category Seminar","author":"Kelly G. Max","unstructured":"G. Max Kelly . 1974. Doctrinal adjunction . In Category Seminar . Springer , 257--280. G. Max Kelly. 1974. Doctrinal adjunction. In Category Seminar. Springer, 257--280."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676969"},{"key":"e_1_3_2_1_18_1","unstructured":"Per Martin-L\u00f6f and Giovanni Sambin. 1984. Intuitionistic type theory. Bibliopolis Naples.  Per Martin-L\u00f6f and Giovanni Sambin. 1984. Intuitionistic type theory. Bibliopolis Naples."},{"key":"e_1_3_2_1_19_1","volume-title":"A List of Successes That Can Change the World","author":"McBride Conor","unstructured":"Conor McBride . 2016. I got plenty o' nuttin '. In A List of Successes That Can Change the World . Springer , 207--233. Available from https:\/\/personal.cis.strath.ac.uk\/conor.mcbride\/PlentyO-CR.pdf. Conor McBride. 2016. I got plenty o' nuttin'. In A List of Successes That Can Change the World. Springer, 207--233. Available from https:\/\/personal.cis.strath.ac.uk\/conor.mcbride\/PlentyO-CR.pdf."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45413-6_27"},{"key":"e_1_3_2_1_21_1","first-page":"112","article-title":"Quantum Programming Languages (Dagstuhl Seminar 18381)","volume":"8","author":"Mosca Michele","year":"2018","unstructured":"Michele Mosca , Martin Roetteler , and Peter Selinger . 2018 . Quantum Programming Languages (Dagstuhl Seminar 18381) . Dagstuhl Reports 8 , 9 (2018), 112 -- 132 . https:\/\/doi.org\/10.4230\/DagRep.8.9.112 10.4230\/DagRep.8.9.112 Michele Mosca, Martin Roetteler, and Peter Selinger. 2018. Quantum Programming Languages (Dagstuhl Seminar 18381). Dagstuhl Reports 8, 9 (2018), 112--132. https:\/\/doi.org\/10.4230\/DagRep.8.9.112","journal-title":"Dagstuhl Reports"},{"key":"e_1_3_2_1_22_1","volume-title":"Chuang","author":"Nielsen Michael A.","year":"2002","unstructured":"Michael A. Nielsen and Isaac L . Chuang . 2002 . Quantum Computation and Quantum Information. Cambridge University Press . Michael A. Nielsen and Isaac L. Chuang. 2002. Quantum Computation and Quantum Information. Cambridge University Press."},{"key":"e_1_3_2_1_23_1","volume-title":"Smith","author":"Nordstr\u00f6m Bengt","year":"1990","unstructured":"Bengt Nordstr\u00f6m , Kent Petersson , and Jan M . Smith . 1990 . Programming in Martin-L\u00f6f's type theory. Oxford University Press Oxford . Bengt Nordstr\u00f6m, Kent Petersson, and Jan M. Smith. 1990. Programming in Martin-L\u00f6f's type theory. Oxford University Press Oxford."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009894"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3122955.3122965"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Robert Rand Jennifer Paykin and Steve Zdancewic. 2018. QWIRE practice: Formal verification of quantum circuits in Coq. (2018). Available from arXiv:1803.00699.  Robert Rand Jennifer Paykin and Steve Zdancewic. 2018. QWIRE practice: Formal verification of quantum circuits in Coq. (2018). Available from arXiv:1803.00699.","DOI":"10.4204\/EPTCS.266.8"},{"key":"e_1_3_2_1_28_1","volume-title":"Proceedings of the 14th International Conference on Quantum Physics and Logic, QPL 2017","author":"Rios Francisco","year":"2017","unstructured":"Francisco Rios and Peter Selinger . 2017 . A categorical model for a quantum circuit description language . In Proceedings of the 14th International Conference on Quantum Physics and Logic, QPL 2017 , Nijmegen, The Netherlands, 3- -7 July 2017. 164--178. Francisco Rios and Peter Selinger. 2017. A categorical model for a quantum circuit description language. In Proceedings of the 14th International Conference on Quantum Physics and Logic, QPL 2017, Nijmegen, The Netherlands, 3--7 July 2017. 164--178."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100061284"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005238"},{"key":"e_1_3_2_1_32_1","volume-title":"UK","author":"V\u00e1k\u00e1r Matthijs","year":"2015","unstructured":"Matthijs V\u00e1k\u00e1r . 2015 . A categorical semantics for linear logical frameworks. In Foundations of Software Science and Computation Structures - 18th International Conference, FoSSaCS 2015. London , UK , April 11-18, 2015. Proceedings. 102--116. Matthijs V\u00e1k\u00e1r. 2015. A categorical semantics for linear logical frameworks. In Foundations of Software Science and Computation Structures - 18th International Conference, FoSSaCS 2015. London, UK, April 11-18, 2015. Proceedings. 102--116."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699415"},{"key":"e_1_3_2_1_34_1","volume-title":"Programming Concepts and Methods","volume":"3","author":"Wadler Philip","year":"1990","unstructured":"Philip Wadler . 1990 . Linear types can change the world! . In Programming Concepts and Methods , Vol. 3 . Citeseer, 5. Philip Wadler. 1990. Linear types can change the world!. In Programming Concepts and Methods, Vol. 3. Citeseer, 5."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75283"}],"event":{"name":"LICS '20: 35th Annual ACM\/IEEE Symposium on Logic in Computer Science","location":"Saarbr\u00fccken Germany","acronym":"LICS '20","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation","EACSL European Association for Computer Science Logic","IEEE-CS\\DATC IEEE Computer Society"]},"container-title":["Proceedings of the 35th Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3373718.3394765","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/abs\/10.1145\/3373718.3394765","content-type":"text\/html","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3373718.3394765","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3373718.3394765","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:35Z","timestamp":1750197755000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3373718.3394765"}},"subtitle":["Extended Abstract"],"short-title":[],"issued":{"date-parts":[[2020,7,8]]},"references-count":33,"alternative-id":["10.1145\/3373718.3394765","10.1145\/3373718"],"URL":"https:\/\/doi.org\/10.1145\/3373718.3394765","relation":{},"subject":[],"published":{"date-parts":[[2020,7,8]]},"assertion":[{"value":"2020-07-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}