{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:39:36Z","timestamp":1770273576303,"version":"3.49.0"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030524814","type":"print"},{"value":"9783030524821","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-52482-1_9","type":"book-chapter","created":{"date-parts":[[2020,7,8]],"date-time":"2020-07-08T16:03:46Z","timestamp":1594224226000},"page":"153-168","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["A Tutorial Introduction to Quantum Circuit Programming in Dependently Typed Proto-Quipper"],"prefix":"10.1007","author":[{"given":"Peng","family":"Fu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kohei","family":"Kishida","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Neil J.","family":"Ross","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Selinger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,7,9]]},"reference":[{"key":"9_CR1","unstructured":"Agda Documentation. \nhttps:\/\/agda.readthedocs.io\/en\/v2.6.0.1\/\n\n. Accessed 01 Feb 2020"},{"key":"9_CR2","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1038\/s41586-019-1666-5","volume":"574","author":"F Arute","year":"2019","unstructured":"Arute, F., et al.: Quantum supremacy using a programmable superconducting processor. Nature 574, 505\u2013510 (2019). (84 authors)","journal-title":"Nature"},{"key":"9_CR3","doi-asserted-by":"publisher","unstructured":"Bove, A., Dybjer, P.: Dependent types at work. In: Bove, A., Barbosa, L.S., Pardo, A., Pinto, J.S. (eds.) LerNet 2008. LNCS, vol. 5520, pp. 57\u201399. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-03153-3_2","DOI":"10.1007\/978-3-642-03153-3_2"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Childs, A.M., Cleve, R., Deotto, E., Farhi, E., Gutmann, S., Spielman, D.A.: Exponential algorithmic speedup by a quantum walk. In: Proceedings of the 35th Annual ACM Symposium on Theory of Computing, pp. 59\u201368 (2003)","DOI":"10.1145\/780542.780552"},{"key":"9_CR5","unstructured":"Circ. \nhttps:\/\/cirq.readthedocs.io\/en\/stable\/\n\n. Accessed 01 Feb 2020"},{"key":"9_CR6","unstructured":"Coq Documentation. \nhttps:\/\/coq.inria.fr\/documentation\/\n\n. Accessed 01 Feb 2020"},{"issue":"1","key":"9_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"JY Girard","year":"1987","unstructured":"Girard, J.Y.: Linear Logic. Theor. Comput. Sci. 50(1), 1\u2013101 (1987)","journal-title":"Theor. Comput. Sci."},{"key":"9_CR8","volume-title":"Proofs and Types","author":"JY Girard","year":"1989","unstructured":"Girard, J.Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge University Press, Cambridge (1989)"},{"key":"9_CR9","doi-asserted-by":"publisher","unstructured":"Green, A.S., Lumsdaine, P.L.F., Ross, N.J., Selinger, P., Valiron, B.: An introduction to quantum programming in Quipper. In: Dueck, G.W., Miller, D.M. (eds.) RC 2013. LNCS, vol. 7948, pp. 110\u2013124. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-38986-3_10","DOI":"10.1007\/978-3-642-38986-3_10"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Green, A.S., Lumsdaine, P.L., Ross, N.J., Selinger, P., Valiron, B.: Quipper: a scalable quantum programming language. In: Proceedings of the 34th Annual ACM SIGPLAN Conference on Programming Language Design and Implementation, vol. 48(6), pp. 333\u2013342. ACM (2013)","DOI":"10.1145\/2499370.2462177"},{"key":"9_CR11","unstructured":"IBM Quantum Experience. \nhttps:\/\/quantum-computing.ibm.com\n\n. Accessed 01 Feb 2020"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/3-540-59451-5_4","volume-title":"Advanced Functional Programming","author":"MP Jones","year":"1995","unstructured":"Jones, M.P.: Functional programming with overloading and higher-order polymorphism. In: Jeuring, J., Meijer, E. (eds.) AFP 1995. LNCS, vol. 925, pp. 97\u2013136. Springer, Heidelberg (1995). \nhttps:\/\/doi.org\/10.1007\/3-540-59451-5_4"},{"key":"9_CR13","volume-title":"Haskell 98 Language and Libraries: The Revised Report","author":"S Peyton Jones","year":"2003","unstructured":"Peyton Jones, S.: Haskell 98 Language and Libraries: The Revised Report. Cambridge University Press, Cambridge (2003)"},{"key":"9_CR14","volume-title":"Introduction to Metamathematics","author":"SC Kleene","year":"1968","unstructured":"Kleene, S.C.: Introduction to Metamathematics. Van Nostrand, New York (1968)"},{"key":"9_CR15","volume-title":"Intuitionistic Type Theory","author":"P Martin-L\u00f6f","year":"1984","unstructured":"Martin-L\u00f6f, P., Sambin, G.: Intuitionistic Type Theory. Bibliopolis, Naples (1984)"},{"issue":"1","key":"9_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1017\/S0956796807006326","volume":"18","author":"C McBride","year":"2008","unstructured":"McBride, C., Paterson, R.: Applicative programming with effects. J. Funct. Program. 18(1), 1\u201313 (2008)","journal-title":"J. Funct. Program."},{"key":"9_CR17","unstructured":"Monroe, C., et al.: Programmable quantum simulations of spin systems with trapped ions (2019). \nhttps:\/\/arxiv.org\/abs\/1912.07845"},{"key":"9_CR18","unstructured":"Mosca, M., Roetteler, M., Selinger, P.: Quantum programming languages (Dagstuhl Seminar 18381). Technical report, Schloss Dagstuhl, Leibniz-Zentrum f\u00fcr Informatik (2019)"},{"key":"9_CR19","volume-title":"Quantum Computation and Quantum Information","author":"MA Nielsen","year":"2002","unstructured":"Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information. Cambridge University Press, Cambridge (2002)"},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"Paykin, J., Rand, R., Zdancewic, S.: QWIRE: a core language for quantum circuits. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, vol. 52(1), pp. 846\u2013858. ACM (2017)","DOI":"10.1145\/3093333.3009894"},{"key":"9_CR21","unstructured":"Peng, F., Kohei, K., Peter, S.: Linear dependent type theory for quantum programming languages. In: Proceedings of the 35th Annual ACM\/IEEE Symposium on Logic in Computer Science. ACM (2020, to appear)"},{"key":"9_CR22","unstructured":"Qiskit. \nhttps:\/\/qiskit.org\/\n\n. Accessed 01 Feb 2020"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Rios, F., Selinger, P.: A categorical model for a quantum circuit description language. Extended abstract. In: Proceedings of the 14th International Workshop on Quantum Physics and Logic, QPL 2017, Nijmegen. Electronic Proceedings in Theoretical Computer Science, vol. 266, pp. 164\u2013178 (2018)","DOI":"10.4204\/EPTCS.266.11"},{"key":"9_CR24","unstructured":"Ross, N.J.: Algebraic and logical methods in quantum computation. Ph. D. thesis, Department of Mathematics and Statistics, Dalhousie University (2015). \nhttps:\/\/arxiv.org\/abs\/1510.02198"},{"issue":"3","key":"9_CR25","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1017\/S0960129506005238","volume":"16","author":"S Peter","year":"2006","unstructured":"Peter, S., Beno\u00eet, V.: A lambda calculus for quantum computation with classical control. Math. Struct. Comput. Sci. 16(3), 527\u2013552 (2006)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9_CR26","unstructured":"Steiger, D.S., H\u00e4ner, T., Troyer, M.: ProjectQ: an open source software framework for quantum computing (2016). \nhttps:\/\/arxiv.org\/abs\/1612.08091"},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"Svore, K., et al.: Q#: Enabling scalable quantum computing and development with a high-level DSL. In: Proceedings of the Real World Domain Specific Languages Workshop, RWDSL 2018. Association for Computing Machinery (2018)","DOI":"10.1145\/3183895.3183901"},{"key":"9_CR28","unstructured":"Wadler, P.: Linear types can change the world. In: Broy, M., Jones, C. (eds.) TC 2 Working Conference on Programming Concepts and Methods, pp. 546\u2013566 (1990)"},{"key":"9_CR29","doi-asserted-by":"crossref","unstructured":"Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad hoc. In: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 60\u201376. ACM (1989)","DOI":"10.1145\/75277.75283"}],"container-title":["Lecture Notes in Computer Science","Reversible Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-52482-1_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,8]],"date-time":"2020-07-08T17:07:22Z","timestamp":1594228042000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-52482-1_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030524814","9783030524821"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-52482-1_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"9 July 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"RC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Reversible Computation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Oslo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Norway","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"rc2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.revcomp.eu\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"50% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}