{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T10:36:04Z","timestamp":1779359764032,"version":"3.51.4"},"reference-count":91,"publisher":"Cambridge University Press (CUP)","issue":"7","license":[{"start":{"date-parts":[[2014,11,17]],"date-time":"2014-11-17T00:00:00Z","timestamp":1416182400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2016,10]]},"abstract":"<jats:p>In this paper, we propose an approach to quantum \u03bb-calculi. The \u2018quantum data-classical control\u2019 paradigm is considered. Starting from a measurement-free untyped quantum \u03bb-calculus called<jats:monospace>Q<\/jats:monospace>, we will study standard properties such as confluence and subject reduction, and some good quantum properties. We will focus on the expressive power, analysing the relationship with other quantum computational models. Successively, we will add an explicit measurement operator to<jats:monospace>Q<\/jats:monospace>. On the resulting calculus, called<jats:monospace>Q<\/jats:monospace>*, we will propose a complete study of reduction sequences regardless of their finiteness, proving confluence results. Moreover, since the stronger motivation behind quantum computing is the research of new results in computational complexity, we will also propose a calculus which captures the three classes of quantum polytime complexity, showing an ICC-like approach in the quantum setting.<\/jats:p>","DOI":"10.1017\/s0960129514000425","type":"journal-article","created":{"date-parts":[[2014,11,17]],"date-time":"2014-11-17T08:45:37Z","timestamp":1416213937000},"page":"1107-1195","source":"Crossref","is-referenced-by-count":25,"title":["On quantum lambda calculi: a foundational perspective"],"prefix":"10.1017","volume":"26","author":[{"given":"MARGHERITA","family":"ZORZI","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,11,17]]},"reference":[{"key":"S0960129514000425_ref65","doi-asserted-by":"publisher","DOI":"10.1201\/9781420012293"},{"key":"S0960129514000425_ref85","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129509990089"},{"key":"S0960129514000425_ref80","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539795293172"},{"key":"S0960129514000425_ref88","volume-title":"To H.B. Curry: Essays on Combinatory Logic, \u03bb-Calculus and Formalism","author":"Wadsworth","year":"1980"},{"key":"S0960129514000425_ref86","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-662-44145-9_1","article-title":"Quantum state transformations and branching distributed temporal logic","volume":"8652","author":"Volpe","year":"2014","journal-title":"Lecture Notes in Computer Science"},{"key":"S0960129514000425_ref89","doi-asserted-by":"publisher","DOI":"10.1038\/299802a0"},{"key":"S0960129514000425_ref70","volume-title":"Computational Complexity","author":"Papadimitriou","year":"1994"},{"key":"S0960129514000425_ref75","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-72831-5"},{"key":"S0960129514000425_ref49","unstructured":"Hashuo I. and Hoshino N. (2011) Semantics of higher-order quantum computation via geometry of interaction. In: Proceedings of 26th Annual Symposium on Logic in Computer Science 237\u2013246."},{"key":"S0960129514000425_ref74","volume-title":"Quantum Information and Computation","author":"Preskill","year":"2006"},{"key":"S0960129514000425_ref53","doi-asserted-by":"crossref","unstructured":"Jain R. , Upadhyay S. and Watrous J. (2009) Two-message quantum interactive proofs are in PSPACE. In: Proceedings of the 50th Annual IEEE Symposium on Foundations of Computer Science, IEEE Computer Society 534\u2013543.","DOI":"10.1109\/FOCS.2009.30"},{"key":"S0960129514000425_ref51","doi-asserted-by":"publisher","DOI":"10.1142\/p001"},{"key":"S0960129514000425_ref61","doi-asserted-by":"publisher","DOI":"10.1109\/ISMVL.2008.36"},{"key":"S0960129514000425_ref19","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539796300921"},{"key":"S0960129514000425_ref84","unstructured":"Vaux L. (2006) Lambda-calculus in an algebraic setting. Research report, Institut de Mathmatiques de Luminy."},{"key":"S0960129514000425_ref59","volume-title":"Quantum Computer Science","author":"Lanzagorta","year":"2009"},{"key":"S0960129514000425_ref16","volume-title":"Quantum Mechanics","author":"Basdevant","year":"2005"},{"key":"S0960129514000425_ref83","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539703432165"},{"key":"S0960129514000425_ref20","volume-title":"Algebra","author":"Birkhoff","year":"1967"},{"key":"S0960129514000425_ref5","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.1"},{"key":"S0960129514000425_ref73","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950600538X"},{"key":"S0960129514000425_ref4","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539705447323"},{"key":"S0960129514000425_ref47","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49208-9_9"},{"key":"S0960129514000425_ref23","volume-title":"Proceedings of Trends in Logic. 50 Years of Studia Logica","author":"Dalla Chiara","year":"2003"},{"key":"S0960129514000425_ref90","unstructured":"Yao A. (1993) Quantum circuit complexity. In: Proceedings of the 34th Annual Symposium on Foundations of Computer Science 352\u2013360."},{"key":"S0960129514000425_ref29","unstructured":"Dal Lago U. and Zorzi M. (2014) Wave-style token machines and quantum lambda calculi. In: Informal Proceedings (with revision) of LINEARITY'14 (FloC'14), 13th July, Vienna 8 pp."},{"key":"S0960129514000425_ref27","doi-asserted-by":"publisher","DOI":"10.1051\/ita\/2012012"},{"key":"S0960129514000425_ref7","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511804090"},{"key":"S0960129514000425_ref42","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"S0960129514000425_ref1","unstructured":"AA.VV. (2013) Website of the QML Project. Available at: http:\/\/fop.cs.nott.ac.uk\/qml\/."},{"key":"S0960129514000425_ref31","article-title":"The measurement calculus","volume":"52","author":"Danos","year":"2007","journal-title":"Journal of the ACM"},{"key":"S0960129514000425_ref37","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRev.47.777"},{"key":"S0960129514000425_ref2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129502003730"},{"key":"S0960129514000425_ref44","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2700"},{"key":"S0960129514000425_ref54","volume-title":"An Introduction to Quantum Computing","author":"Kaye","year":"2007"},{"key":"S0960129514000425_ref64","unstructured":"Maymin P. (1997) The lambda-q calculus can efficiently simulate quantum computers. ArXiv:quant-ph\/9702057. Unpublished."},{"key":"S0960129514000425_ref79","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1994.365700"},{"key":"S0960129514000425_ref8","first-page":"59","article-title":"Measurements and confluence in quantum Lambda calculi with explicit qubits","volume":"270","author":"Arrighi","year":"2008","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"S0960129514000425_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2010.10.002"},{"key":"S0960129514000425_ref68","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00111-6"},{"key":"S0960129514000425_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/BF01011339"},{"key":"S0960129514000425_ref22","volume-title":"A Course in Functional Analysis","author":"Conway","year":"1990"},{"key":"S0960129514000425_ref87","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58027-1_24"},{"key":"S0960129514000425_ref48","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12821-9_5"},{"key":"S0960129514000425_ref82","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_17"},{"key":"S0960129514000425_ref15","volume-title":"The lambda calculus: its Syntax and Semantics","author":"Barebdregt","year":"1984"},{"key":"S0960129514000425_ref25","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.07.045"},{"key":"S0960129514000425_ref50","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-09636-9"},{"key":"S0960129514000425_ref18","doi-asserted-by":"publisher","DOI":"10.1038\/scientificamerican0785-48"},{"key":"S0960129514000425_ref11","unstructured":"Arrighi P. and Dowek G. (2008) Linear-algebraic lambda-calculus: Higher-order, encodings and confluence. In: Proceedings of the 19th Annual Conference on Term Rewriting and Applications 17\u201331."},{"key":"S0960129514000425_ref58","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.10.018"},{"key":"S0960129514000425_ref63","unstructured":"Maymin P. (1996) Extending the \u03bb-calculus to express randomized and quantumized algorithms. ArXiv:quant-ph\/9612052. Unpublished."},{"key":"S0960129514000425_ref52","article-title":"QIP=PSPACE","volume":"58","author":"Jain","year":"2011","journal-title":"Journal of the ACM"},{"key":"S0960129514000425_ref43","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90386-T"},{"key":"S0960129514000425_ref81","first-page":"116","article-title":"On the power of quantum computation","volume":"26","author":"Simon","year":"1994","journal-title":"SIAM Journal on Computing"},{"key":"S0960129514000425_ref69","doi-asserted-by":"publisher","DOI":"10.1007\/s11128-008-0091-8"},{"key":"S0960129514000425_ref35","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.01.005"},{"key":"S0960129514000425_ref77","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005238"},{"key":"S0960129514000425_ref72","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.12.015"},{"key":"S0960129514000425_ref45","unstructured":"Grattage J. (2006) A Functional Quantum Programming Language, Ph.D. thesis, University of Nottingham."},{"key":"S0960129514000425_ref40","unstructured":"Gay S. (2011) Bibliography on quantum programming languages. Available at: http:\/\/www.dcs.gla.ac.uk\/simon\/quantum\/."},{"key":"S0960129514000425_ref46","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.01.015"},{"key":"S0960129514000425_ref55","doi-asserted-by":"publisher","DOI":"10.1090\/gsm\/047"},{"key":"S0960129514000425_ref39","article-title":"An implicit characterization of PSPACE","volume":"13","author":"Gaboardi","year":"2013","journal-title":"ACM Transactions on Computational Logic"},{"key":"S0960129514000425_ref36","first-page":"97","article-title":"Quantum theory, the Church\u2013Turing principle and the universal quantum computer","volume":"A400","author":"Dirac","year":"1947","journal-title":"Proceedings of the Royal Society of London A"},{"key":"S0960129514000425_ref76","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004256"},{"key":"S0960129514000425_ref91","unstructured":"Zorzi M. (2009) Lambda Calculi and Logics for Quantum Computing, Ph.D. thesis, Dipartimento di Informatica, Universit\u00e0 degli Studi di Verona."},{"key":"S0960129514000425_ref56","doi-asserted-by":"publisher","DOI":"10.1215\/S0012-7094-36-00227-2"},{"key":"S0960129514000425_ref24","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950800741X"},{"key":"S0960129514000425_ref66","doi-asserted-by":"publisher","DOI":"10.1016\/S0375-9601(02)01803-0"},{"key":"S0960129514000425_ref10","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.88.1"},{"key":"S0960129514000425_ref38","doi-asserted-by":"publisher","DOI":"10.1007\/BF02650179"},{"key":"S0960129514000425_ref41","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139193313"},{"key":"S0960129514000425_ref3","doi-asserted-by":"crossref","unstructured":"Aharonov D. , Kitaev A. and Nisan N. (1998) Quantum circuits with mixed states. In: Proceedings of the 30th Annual ACM Symposium on the Theory of Computing 20\u201330.","DOI":"10.1145\/276698.276708"},{"key":"S0960129514000425_ref57","doi-asserted-by":"crossref","unstructured":"Knill E. (1996) Conventions for quantum pseudocode. Technical Report LAUR-96-2724, Los Alamos National Laboratory.","DOI":"10.2172\/366453"},{"key":"S0960129514000425_ref26","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.01.035"},{"key":"S0960129514000425_ref21","doi-asserted-by":"publisher","DOI":"10.1145\/190616.190617"},{"key":"S0960129514000425_ref28","unstructured":"Dal Lago U. and Zorzi M. (2013) Wave-style token machines and quantum lambda calculi. Long version available at: http:\/\/arxiv.org\/abs\/1307.0550."},{"key":"S0960129514000425_ref60","volume-title":"Fisica moderna. Meccanica quantistica, caos e sistemi complessi","author":"Maccone","year":"2008"},{"key":"S0960129514000425_ref33","doi-asserted-by":"publisher","DOI":"10.1098\/rspa.1985.0070"},{"key":"S0960129514000425_ref6","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.12.010"},{"key":"S0960129514000425_ref32","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139193313.008"},{"key":"S0960129514000425_ref9","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(1:11)2012"},{"key":"S0960129514000425_ref34","doi-asserted-by":"publisher","DOI":"10.2307\/421056"},{"key":"S0960129514000425_ref62","first-page":"475","article-title":"Modal deduction systems for quantum state transformations","volume":"17","author":"Masini","year":"2011","journal-title":"Multiple-Valued Logic and Soft Computing"},{"key":"S0960129514000425_ref71","unstructured":"Perdrix S. (2006) Mod\u00e8les formels du calcul quantique: Ressources, machines abstraites et calcul par mesure, Ph.D. thesis, Institut National Polytechnique de Grenoble."},{"key":"S0960129514000425_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24727-2_4"},{"key":"S0960129514000425_ref67","volume-title":"Physical Review","author":"Nielsen","year":"2000"},{"key":"S0960129514000425_ref30","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.12.012"},{"key":"S0960129514000425_ref78","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139193313.005"},{"key":"S0960129514000425_ref13","doi-asserted-by":"crossref","DOI":"10.1145\/1555746.1555747","article-title":"Special issue on implicit complexity","volume":"10","author":"Baillot","year":"2009","journal-title":"ACM Transactions on Computational Logic"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129514000425","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,26]],"date-time":"2020-08-26T23:00:07Z","timestamp":1598482807000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129514000425\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,17]]},"references-count":91,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2016,10]]}},"alternative-id":["S0960129514000425"],"URL":"https:\/\/doi.org\/10.1017\/s0960129514000425","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,11,17]]}}}