{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:34:13Z","timestamp":1767929653613,"version":"3.49.0"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031908965","type":"print"},{"value":"9783031908972","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>The two main notions of control in quantum programming languages are\u00a0often referred to as \u201cquantum\u201d control and \u201cclassical\u201d control. With the latter, the control flow is based on classical information, potentially resulting\u00a0from a quantum measurement, and this paradigm is well-suited to mixed state quantum computation. Whereas with quantum control, we are primarily focused on\u00a0pure quantum computation and there the \u201ccontrol\u201d is based on superposition. \u00a0The two paradigms have not mixed well traditionally and they are almost always treated separately. In this work, we show that the paradigms may be combined within the same system. The key ingredients for achieving this are:\u00a0(1) syntactically: a modality for incorporating pure quantum types into a\u00a0mixed state quantum type system; (2) operationally: an adaptation of the notion\u00a0of \u201cquantum configuration\u201d from quantum lambda-calculi, where the quantum\u00a0data is replaced with pure quantum primitives; (3) denotationally: suitable (sub)categories of Hilbert spaces, for pure computation and von Neumann algebras, for mixed state computation in the Heisenberg picture of quantum mechanics.<\/jats:p>","DOI":"10.1007\/978-3-031-90897-2_8","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:18:21Z","timestamp":1746001101000},"page":"155-175","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Combining quantum and classical control: syntax, semantics and adequacy"],"prefix":"10.1007","author":[{"given":"Kinnari","family":"Dave","sequence":"first","affiliation":[]},{"given":"Louis","family":"Lemonnier","sequence":"additional","affiliation":[]},{"given":"Romain","family":"P\u00e9choux","sequence":"additional","affiliation":[]},{"given":"Vladimir","family":"Zamdzhiev","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"8_CR1","unstructured":"Andr\u00e9s-Mart\u00ednez, P.: Unbounded loops in quantum programs: categories and weak-while loops. Ph.D. thesis, Laboratory for Foundations of Computer Science, School of Informatics, University of Edinburgh (2022). https:\/\/doi.org\/10.48550\/arXiv.2212.05371"},{"key":"8_CR2","doi-asserted-by":"publisher","unstructured":"Arrighi, P., Dowek, G.: Lineal: A linear-algebraic lambda-calculus. Log. Methods Comput. Sci. 13(1) (2017). https:\/\/doi.org\/10.23638\/LMCS-13(1:8)2017, https:\/\/doi.org\/10.23638\/LMCS-13(1:8)2017","DOI":"10.23638\/LMCS-13(1:8)2017"},{"key":"8_CR3","unstructured":"Chardonnet, K.: Towards a Curry-Howard Correspondence for Quantum Computation. (Vers une correspondance de Curry-Howard pour le calcul quantique). Ph.D. thesis, Universit\u00e9 Paris-Saclay, France (2023), https:\/\/tel.archives-ouvertes.fr\/tel-03959403"},{"key":"8_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 thirty-fifth annual ACM symposium on Theory of computing. pp. 59\u201368 (2003)","DOI":"10.1145\/780542.780552"},{"key":"8_CR5","doi-asserted-by":"publisher","unstructured":"Cho, K.: Semantics for a quantum programming language by operator algebras. Electronic Proceedings in Theoretical Computer Science 172, 165\u2013190 (Dec 2014). https:\/\/doi.org\/10.4204\/eptcs.172.12, http:\/\/dx.doi.org\/10.4204\/EPTCS.172.12","DOI":"10.4204\/eptcs.172.12"},{"key":"8_CR6","unstructured":"Cho, K., Westerbaan, A.: Von Neumann Algebras form a Model for the Quantum Lambda Calculus (2016). https:\/\/doi.org\/10.48550\/arXiv.1603.02133"},{"key":"8_CR7","doi-asserted-by":"publisher","unstructured":"Clairambault, P., de\u00a0Visme, M.: Full abstraction for the quantum lambda-calculus. Proc. ACM Program. Lang. 4(POPL), 63:1\u201363:28 (2020). https:\/\/doi.org\/10.1145\/3371131, https:\/\/doi.org\/10.1145\/3371131","DOI":"10.1145\/3371131"},{"key":"8_CR8","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":"8_CR9","doi-asserted-by":"publisher","unstructured":"D\u00edaz-Caro, A., Malherbe, O.: Semimodules and the (syntactically-)linear lambda calculus. CoRR abs\/2205.02142 (2022). https:\/\/doi.org\/10.48550\/ARXIV.2205.02142, https:\/\/doi.org\/10.48550\/arXiv.2205.02142","DOI":"10.48550\/ARXIV.2205.02142"},{"key":"8_CR10","doi-asserted-by":"publisher","unstructured":"D\u00edaz-Caro, A., Guillermo, M., Miquel, A., Valiron, B.: Realizability in the unitary sphere. In: LICS 2019. IEEE (jun 2019). https:\/\/doi.org\/10.1109\/lics.2019.8785834, https:\/\/doi.org\/10.1109%2Flics.2019.8785834","DOI":"10.1109\/lics.2019.8785834"},{"key":"8_CR11","doi-asserted-by":"publisher","unstructured":"D\u00edaz-Caro, A., Malherbe, O.: Quantum control in the unitary sphere: Lambda-s1 and its categorical model. Logical Methods in Computer Science Volume 18, Issue 3 (2022). https:\/\/doi.org\/10.46298\/lmcs-18(3:32)2022, https:\/\/doi.org\/10.46298%2Flmcs-18%283%3A32%292022","DOI":"10.46298\/lmcs-18(3:32)2022"},{"key":"8_CR12","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 ACM SIGPLAN conference on Programming language design and implementation. pp. 333\u2013342 (2013)","DOI":"10.1145\/2491956.2462177"},{"key":"8_CR13","doi-asserted-by":"publisher","unstructured":"Jia, X., Kornell, A., Lindenhovius, B., Mislove, M.W., Zamdzhiev, V.: Semantics for variational quantum programming. In: POPL 2022. vol.\u00a06, pp. 1\u201331. ACM (2022). https:\/\/doi.org\/10.1145\/3498687","DOI":"10.1145\/3498687"},{"key":"8_CR14","unstructured":"Lemonnier, L.: The Semantics of Effects : Centrality, Quantum Control and Reversible Recursion. Theses, Universit\u00e9 Paris-Saclay (Jun 2024), https:\/\/theses.hal.science\/tel-04625771"},{"key":"8_CR15","doi-asserted-by":"publisher","unstructured":"Pagani, M., Selinger, P., Valiron, B.: Applying quantitative semantics to higher-order quantum computing. In: POPL 2014. pp. 647\u2013658. ACM (2014). https:\/\/doi.org\/10.1145\/2535838.2535879","DOI":"10.1145\/2535838.2535879"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Paykin, J., Rand, R., Zdancewic, S.: Qwire: a core language for quantum circuits. ACM SIGPLAN Notices 52(1), 846\u2013858 (2017)","DOI":"10.1145\/3093333.3009894"},{"key":"8_CR17","doi-asserted-by":"publisher","unstructured":"P\u00e9choux, R., Perdrix, S., Rennela, M., Zamdzhiev, V.: Quantum programming with inductive datatypes: Causality and affine type theory. In: FoSSaCS 2020. Lecture Notes in Computer Science, vol. 12077, pp. 562\u2013581. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-45231-5_29","DOI":"10.1007\/978-3-030-45231-5_29"},{"key":"8_CR18","doi-asserted-by":"publisher","unstructured":"Sabry, A., Valiron, B., Vizzotto, J.K.: From symmetric pattern-matching to quantum control. In: FoSSaCS 2018). Lecture Notes in Computer Science, vol. 10803, pp. 348\u2013364. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89366-2_19","DOI":"10.1007\/978-3-319-89366-2_19"},{"key":"8_CR19","doi-asserted-by":"crossref","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":"8_CR20","doi-asserted-by":"publisher","unstructured":"Selinger, P., Valiron, B.: A lambda calculus for quantum computation with classical control. Mathematical Structures in Computer Science 16(3), 527\u2013552 (2006). https:\/\/doi.org\/10.1017\/S0960129506005238","DOI":"10.1017\/S0960129506005238"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"Selinger, P., Valiron, B., et\u00a0al.: Quantum lambda calculus. Semantic techniques in quantum computation pp. 135\u2013172 (2009)","DOI":"10.1017\/CBO9781139193313.005"},{"key":"8_CR22","doi-asserted-by":"publisher","unstructured":"Tsukada, T., Asada, K.: Enriched presheaf model of quantum FPC. Proc. ACM Program. Lang. 8(POPL), 362\u2013392 (2024). https:\/\/doi.org\/10.1145\/3632855, https:\/\/doi.org\/10.1145\/3632855","DOI":"10.1145\/3632855"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Valiron, B.: Semantics of quantum programming languages: Classical control, quantum control. Journal of Logical and Algebraic Methods in Programming 128 (2022). https:\/\/doi.org\/10.1016\/j.jlamp.2022.100790","DOI":"10.1016\/j.jlamp.2022.100790"},{"key":"8_CR24","unstructured":"de\u00a0Visme, M.: Quantum Game Semantics. (S\u00e9mantique des Jeux Quantique). Ph.D. thesis, University of Lyon, France (2020), https:\/\/tel.archives-ouvertes.fr\/tel-03045844"},{"key":"8_CR25","doi-asserted-by":"publisher","unstructured":"Voichick, F., Li, L., Rand, R., Hicks, M.: Qunity: A unified language for quantum and classical computing. Proc. ACM Program. Lang. 7(POPL), 921\u2013951 (2023). https:\/\/doi.org\/10.1145\/3571225, https:\/\/doi.org\/10.1145\/3571225","DOI":"10.1145\/3571225"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90897-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:18:29Z","timestamp":1746001109000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90897-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031908965","9783031908972"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90897-2_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","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":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/fossacs\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}