{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T07:53:42Z","timestamp":1770278022595,"version":"3.49.0"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030452308","type":"print"},{"value":"9783030452315","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":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Inductive datatypes in programming languages allow users to define useful data structures such as natural numbers, lists, trees, and others. In this paper we show how inductive datatypes may be added to the quantum programming language QPL. We construct a sound categorical model for the language and by doing so we provide the first detailed semantic treatment of user-defined inductive datatypes in quantum programming. We also show our denotational interpretation is invariant with respect to big-step reduction, thereby establishing another novel result for quantum programming. Compared to classical programming, this property is considerably more difficult to prove and we demonstrate its usefulness by showing how it immediately implies computational adequacy at all types. To further cement our results, our semantics is entirely based on a physically natural model of von Neumann algebras, which are mathematical structures used by physicists to study quantum mechanics.<\/jats:p>","DOI":"10.1007\/978-3-030-45231-5_29","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T10:02:53Z","timestamp":1587117773000},"page":"562-581","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Quantum Programming with Inductive Datatypes: Causality and Affine Type Theory"],"prefix":"10.1007","author":[{"given":"Romain","family":"P\u00e9choux","sequence":"first","affiliation":[]},{"given":"Simon","family":"Perdrix","sequence":"additional","affiliation":[]},{"given":"Mathys","family":"Rennela","sequence":"additional","affiliation":[]},{"given":"Vladimir","family":"Zamdzhiev","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"key":"29_CR1","doi-asserted-by":"publisher","unstructured":"Abadi, M., Fiore, M.P.: Syntactic Considerations on Recursive Types. In: Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996. pp. 242\u2013252. IEEE Computer Society (1996). https:\/\/doi.org\/10.1109\/LICS.1996.561324","DOI":"10.1109\/LICS.1996.561324"},{"key":"29_CR2","unstructured":"Cho, K.: Semantics for a Quantum Programming Language by Operator Algebras (2014), Master Thesis, University of Tokyo."},{"key":"29_CR3","doi-asserted-by":"publisher","unstructured":"Cho, K.: Semantics for a Quantum Programming Language by Operator Algebras. New Generation Comput. 34(1-2), 25\u201368 (2016). https:\/\/doi.org\/10.1007\/s00354-016-0204-3","DOI":"10.1007\/s00354-016-0204-3"},{"key":"29_CR4","unstructured":"Cho, K., Westerbaan, A.: Von Neumann Algebras form a Model for the Quantum Lambda Calculus (2016), http:\/\/arxiv.org\/abs\/1603.02133, manuscript."},{"key":"29_CR5","doi-asserted-by":"publisher","unstructured":"Clairambault, P., de\u00a0Visme, M., Winskel, G.: Game semantics for quantum programming. PACMPL 3(POPL), 32:1\u201332:29 (2019). https:\/\/doi.org\/10.1145\/3290345","DOI":"10.1145\/3290345"},{"key":"29_CR6","unstructured":"Fiore, M.P.: Axiomatic Domain Theory in Categories of Partial Maps. Ph.D. thesis, University of Edinburgh, UK (1994)"},{"key":"29_CR7","doi-asserted-by":"publisher","unstructured":"Gay, S.J.: Quantum programming languages: survey and bibliography. Mathematical Structures in Computer Science 16(4), 581\u2013600 (2006). https:\/\/doi.org\/10.1017\/S0960129506005378","DOI":"10.1017\/S0960129506005378"},{"key":"29_CR8","doi-asserted-by":"publisher","unstructured":"Harrow, A.W., Hassidim, A., Lloyd, S.: Quantum Algorithm for Linear Systems of Equations. Phys. Rev. Lett. 103, 150502 (Oct 2009). https:\/\/doi.org\/10.1103\/PhysRevLett.103.150502","DOI":"10.1103\/PhysRevLett.103.150502"},{"key":"29_CR9","doi-asserted-by":"publisher","unstructured":"Hasuo, I., Hoshino, N.: Semantics of higher-order quantum computation via geometry of interaction. Ann. Pure Appl. Logic 168(2), 404\u2013469 (2017). https:\/\/doi.org\/10.1016\/j.apal.2016.10.010","DOI":"10.1016\/j.apal.2016.10.010"},{"key":"29_CR10","doi-asserted-by":"publisher","unstructured":"Kissinger, A., Uijlen, S.: A categorical semantics for causal structure. In: 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017. pp. 1\u201312. IEEE Computer Society (2017). https:\/\/doi.org\/10.1109\/LICS.2017.8005095","DOI":"10.1109\/LICS.2017.8005095"},{"key":"29_CR11","doi-asserted-by":"publisher","unstructured":"Kornell, A.: Quantum collections. International Journal of Mathematics 28(12), 1750085 (2017). https:\/\/doi.org\/10.1142\/S0129167X17500859","DOI":"10.1142\/S0129167X17500859"},{"key":"29_CR12","unstructured":"Lago, U.D., Faggian, C., Valiron, B., Yoshimizu, A.: The geometry of parallelism: classical, probabilistic, and quantum effects. In: Castagna,G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. pp. 833\u2013845. ACM (2017), http:\/\/dl.acm.org\/citation.cfm?id=3009859"},{"key":"29_CR13","unstructured":"Lindenhovius, B., Mislove, M., Zamdzhiev, V.: LNL-FPC: The Linear\/Non-linear Fixpoint Calculus https:\/\/arxiv.org\/abs\/1906.09503, submitted."},{"key":"29_CR14","doi-asserted-by":"publisher","unstructured":"Lindenhovius, B., Mislove, M., Zamdzhiev, V.: Mixed linear and non-linear recursive types. Proc. ACM Program. Lang. 3(ICFP), 111:1\u2013111:29 (Jul 2019). https:\/\/doi.org\/10.1145\/3341715","DOI":"10.1145\/3341715"},{"key":"29_CR15","doi-asserted-by":"publisher","unstructured":"Lindenhovius, B., Mislove, M.W., Zamdzhiev, V.: Enriching a Linear\/Non-linear Lambda Calculus: A Programming Language for String Diagrams. In: Dawar, A., Gr\u00e4del, E. (eds.) Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018. pp. 659\u2013668. ACM (2018). https:\/\/doi.org\/10.1145\/3209108.3209196","DOI":"10.1145\/3209108.3209196"},{"key":"29_CR16","doi-asserted-by":"publisher","unstructured":"Mosca, M., Roetteler, M., Selinger, P.: Quantum Programming Languages (Dagstuhl Seminar 18381). Dagstuhl Reports 8(9), 112\u2013132 (2019). https:\/\/doi.org\/10.4230\/DagRep.8.9.112","DOI":"10.4230\/DagRep.8.9.112"},{"key":"29_CR17","doi-asserted-by":"publisher","unstructured":"Pagani, M., Selinger, P., Valiron, B.: Applying quantitative semantics to higher-order quantum computing. In: Jagannathan, S., Sewell, P. (eds.) The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201914, San Diego, CA, USA, January 20-21, 2014. pp. 647\u2013658. ACM (2014). https:\/\/doi.org\/10.1145\/2535838.2535879","DOI":"10.1145\/2535838.2535879"},{"key":"29_CR18","doi-asserted-by":"publisher","unstructured":"Perdrix, S.: Quantum Entanglement Analysis Based on Abstract Interpretation. In: Alpuente, M., Vidal, G. (eds.) Static Analysis, 15th International Symposium, SAS 2008, Valencia, Spain, July 16-18, 2008. Proceedings. Lecture Notes in Computer Science, vol.\u00a05079, pp. 270\u2013282. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-69166-2_18","DOI":"10.1007\/978-3-540-69166-2_18"},{"key":"29_CR19","unstructured":"Rennela, M.: Operator Algebras in Quantum Computation (2013), Master Thesis, Universit\u00e9 Paris 7 Denis Diderot."},{"key":"29_CR20","doi-asserted-by":"publisher","unstructured":"Rennela, M., Staton, S.: Classical Control and Quantum Circuits in Enriched Category Theory. Electr. Notes Theor. Comput. Sci. 336, 257\u2013279 (2018). https:\/\/doi.org\/10.1016\/j.entcs.2018.03.027","DOI":"10.1016\/j.entcs.2018.03.027"},{"key":"29_CR21","doi-asserted-by":"publisher","unstructured":"Rios, F., Selinger, P.: A Categorical Model for a Quantum Circuit Description Language. In: QPL (2017). https:\/\/doi.org\/10.4204\/EPTCS.266.11","DOI":"10.4204\/EPTCS.266.11"},{"key":"29_CR22","unstructured":"Ross, N.J.: Algebraic and Logical Methods in Quantum Computation (2015), Ph.D. thesis, Dalhousie University."},{"key":"29_CR23","doi-asserted-by":"publisher","unstructured":"Selinger, P.: Towards a quantum programming language. Mathematical Structures in Computer Science 14(4), 527\u2013586 (2004). https:\/\/doi.org\/10.1017\/S0960129504004256","DOI":"10.1017\/S0960129504004256"},{"key":"29_CR24","doi-asserted-by":"publisher","unstructured":"Shor, P.W.: Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer. SIAM Review 41(2), 303\u2013332 (1999). https:\/\/doi.org\/10.1137\/S0036144598347011","DOI":"10.1137\/S0036144598347011"},{"key":"29_CR25","doi-asserted-by":"crossref","unstructured":"Takesaki, M.: Theory of Operator Algebras. Vol. I, II and III. Springer-Verlag, Berlin (2002)","DOI":"10.1007\/978-3-662-10453-8"},{"key":"29_CR26","doi-asserted-by":"publisher","unstructured":"Westerbaan, A.: Quantum Programs as Kleisli Maps. In: Duncan, R., Heunen, C.(eds.) Proceedings 13th International Conference on Quantum Physics and Logic, QPL 2016, Glasgow, Scotland, 6-10 June 2016. EPTCS, vol.\u00a0236, pp. 215\u2013228 (2016). https:\/\/doi.org\/10.4204\/EPTCS.236.14","DOI":"10.4204\/EPTCS.236.14"},{"key":"29_CR27","unstructured":"Westerbaan, B.: Dagger and Dilation in the Category of Von Neumann algebras. Ph.D. thesis, Radboud University (2018), http:\/\/arxiv.org\/abs\/1803.01911"},{"key":"29_CR28","doi-asserted-by":"crossref","unstructured":"Wootters, W.K., Zurek, W.H.: A single quantum cannot be cloned. Nature 299(5886), 802\u2013803 (1982)","DOI":"10.1038\/299802a0"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-45231-5_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,1,7]],"date-time":"2021-01-07T14:06:33Z","timestamp":1610028393000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-45231-5_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030452308","9783030452315"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-45231-5_29","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":"17 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","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":"25 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-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":"98","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":"31","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":"32% - 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":"12","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 could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","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)"}}]}}