{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,11]],"date-time":"2025-12-11T12:48:14Z","timestamp":1765457294068,"version":"3.46.0"},"reference-count":29,"publisher":"Oxford University Press (OUP)","issue":"8","license":[{"start":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T00:00:00Z","timestamp":1762214400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/pages\/standard-publication-reuse-rights"}],"funder":[{"DOI":"10.13039\/501100000780","name":"European Union","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"publisher"}]},{"name":"MSCA SE project QCOMICAL","award":["101182520"],"award-info":[{"award-number":["101182520"]}]},{"name":"Plan France 2030"},{"name":"EPiQ","award":["ANR-22-PETQ-0007"],"award-info":[{"award-number":["ANR-22-PETQ-0007"]}]},{"name":"Uruguayan CSIC","award":["22520220100073UD"],"award-info":[{"award-number":["22520220100073UD"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025,11,4]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>We introduce the ${{\\mathcal L}_!^{\\mathcal S}}$-calculus, a linear lambda-calculus extended with scalar multiplication and term addition, that acts as a proof language for intuitionistic linear logic. These algebraic operations enable the direct expression of linearity at the syntactic level, a property not typically available in standard proof-term calculi. Building upon previous work, we develop the ${{\\mathcal L}_{!}^{\\mathcal S}}$-calculus as an extension of the ${\\mathcal L}^{\\mathcal S}$-calculus with the ! modality. We prove key meta-theoretical properties\u2014subject reduction, confluence, strong normalization and an introduction property\u2014as well as preserve the expressiveness of the original ${\\mathcal L}^{\\mathcal S}$-calculus, including the encoding of vectors and matrices, and the correspondence between proof-terms and linear functions. A denotational semantics is provided in the framework of linear categories with biproducts, ensuring a sound and adequate interpretation of the calculus. This work is part of a broader programme aiming to build a measurement-free quantum programming language grounded in linear logic.<\/jats:p>","DOI":"10.1093\/logcom\/exaf053","type":"journal-article","created":{"date-parts":[[2025,11,9]],"date-time":"2025-11-09T10:40:01Z","timestamp":1762684801000},"source":"Crossref","is-referenced-by-count":0,"title":["An algebraic extension of intuitionistic linear logic: the \ud835\udcdb!\ud835\udcae-calculus and its categorical model"],"prefix":"10.1093","volume":"35","author":[{"given":"Alejandro","family":"D\u00edaz-Caro","sequence":"first","affiliation":[{"name":"Universit\u00e9 de Lorraine, CNRS, Inria, LORIA , 615 rue du Jardin Botanique, F54506 Vandoeuvre-l\u00e8s-Nancy ,","place":["France"]},{"name":"Universidad Nacional de Quilmes, DCyT , Roque S\u00e1enz Pe\u00f1a 352, 1876, Bernal, PBA ,","place":["Argentina"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Malena","family":"Ivnisky","sequence":"additional","affiliation":[{"name":"Universidad de Buenos Aires, DC, FCEyN, Pabell\u00f3n 0+Inf, Ciudad Universitaria , 1428, Buenos Aires ,","place":["Argentina"]},{"name":"Universidad de Buenos Aires-CONICET, ICC, Pabell\u00f3n 0+Inf, Ciudad Universitaria , 1428, Buenos Aires ,","place":["Argentina"]},{"name":"Universidad de la Rep\u00fablica\u2013MEC, PEDECIBA , Isidoro de Mar\u00eda 1614, P6, 11800, Montevideo ,","place":["Uruguay"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Octavio","family":"Malherbe","sequence":"additional","affiliation":[{"name":"Universidad de la Rep\u00fablica, IMERL , FIng, Julio Herrera y Reissig 565, 11200, Montevideo ,","place":["Uruguay"]}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2025,11,8]]},"reference":[{"key":"2025121107432355700_ref1","first-page":"249","article-title":"A functional quantum programming language","volume-title":"Proceedings of LICS 2005","author":"Altenkirch","year":"2005"},{"key":"2025121107432355700_ref2","article-title":"A system F accounting for scalars","volume":"8","author":"Arrighi","year":"2012","journal-title":"Logical Methods in Computer Science"},{"key":"2025121107432355700_ref3","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1016\/j.ic.2017.04.001","article-title":"The vectorial lambda-calculus","volume":"254","author":"Arrighi","year":"2017","journal-title":"Information and Computation"},{"key":"2025121107432355700_ref4","article-title":"Lineal: a linear-algebraic lambda-calculus","volume":"13","author":"Arrighi","year":"2017","journal-title":"Logical Methods in Computer Science"},{"key":"2025121107432355700_ref5","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1017\/S0960129500001274","article-title":"$\\ast $-autonomous categories and linear logic","volume":"1","author":"Barr","year":"1991","journal-title":"Mathematical Structures in Computer Science"},{"key":"2025121107432355700_ref6","first-page":"1887","article-title":"Cat\u00e9gories avec multiplication","volume":"256","author":"B\u00e9nabou","year":"1963","journal-title":"Comptes Rendus des S\u00e9ances de l\u2019Acad\u00e9mie des Sciences"},{"volume-title":"On Intuitionistic Linear Logic","year":". 1994","author":"Bierman","key":"2025121107432355700_ref7"},{"volume-title":"Dual Intuitionistic Linear Logic","year":". 1996","author":"Bierman","key":"2025121107432355700_ref8"},{"key":"2025121107432355700_ref9","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1006\/inco.1994.1003","article-title":"Lambda-calculi for (strict) parallel functions","volume":"108","author":"Boudol","year":"1994","journal-title":"Information and Computation"},{"volume-title":"The Many-Worlds Calculus. Logical Methods in Computer Science","year":"2025","author":"Chardonnet","key":"2025121107432355700_ref10"},{"key":"2025121107432355700_ref11","doi-asserted-by":"crossref","DOI":"10.1017\/9781316219317","volume-title":"Picturing Quantum Processes: A First Course in Quantum Theory and Diagrammatic Reasoning","author":"Coecke","year":"2017"},{"volume-title":"Categories for Types","year":"1993","author":"Crole","key":"2025121107432355700_ref12"},{"key":"2025121107432355700_ref13","doi-asserted-by":"crossref","DOI":"10.1016\/j.tcs.2023.113840","article-title":"A new connective in natural deduction, and its application to quantum computing","volume":"957","author":"D\u00edaz-Caro","year":"2023","journal-title":"Theoretical Computer Science"},{"key":"2025121107432355700_ref14","doi-asserted-by":"crossref","first-page":"1103","DOI":"10.1017\/S0960129524000197","article-title":"A linear linear lambda-calculus","volume":"34","author":"D\u00edaz-Caro","year":"2024","journal-title":"Mathematical Structures in Computer Science"},{"key":"2025121107432355700_ref15","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1007\/978-3-031-62687-6_2","article-title":"A linear proof language for second-order intuitionistic linear logic","volume-title":"Logic, Language, Information and Computation","author":"D\u00edaz-Caro","year":"2024"},{"key":"2025121107432355700_ref16","doi-asserted-by":"crossref","first-page":"104012","DOI":"10.1016\/j.biosystems.2019.104012","article-title":"Two linearities for quantum computing in the lambda calculus","volume":"186","author":"D\u00edaz-Caro","year":"2019","journal-title":"BioSystems"},{"key":"2025121107432355700_ref17","first-page":"1","article-title":"Realizability in the unitary sphere","author":"D\u00edaz-Caro","year":"2019","journal-title":"Proceedings of LICS, 2019"},{"key":"2025121107432355700_ref18","article-title":"Quantum control in the unitary sphere: Lambda-${S}\\_1$ and its categorical model","volume":"18","author":"D\u00edaz-Caro","year":"2022","journal-title":"Logical Methods in Computer Science"},{"article-title":"Semimodules and the (syntactically-)linear lambda calculus","year":"2022","author":"D\u00edaz-Caro","key":"2025121107432355700_ref19"},{"article-title":"The sup connective in IMALL: a categorical semantics","year":"2024","author":"D\u00edaz-Caro","key":"2025121107432355700_ref20"},{"key":"2025121107432355700_ref21","doi-asserted-by":"crossref","first-page":"421","DOI":"10.1007\/978-3-642-99902-4_22","article-title":"Closed categories","volume-title":"Proceedings of the Conference on Categorical Algebra","author":"Eilenberg","year":"1966"},{"volume-title":"Interpr\u00e9tation Fonctionnelle et \u00e9limination Des Coupures Dans L\u2019arith-m\u00e9tique d\u2019ordre sup\u00e9rieure","year":"1972","author":"Girard","key":"2025121107432355700_ref22"},{"key":"2025121107432355700_ref23","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","article-title":"Linear logic","volume":"50","author":"Girard","year":"1987","journal-title":"Theoretical Computer Science"},{"volume-title":"Models of Linear Polymorphism","year":"2004","author":"Maneggia","key":"2025121107432355700_ref24"},{"key":"2025121107432355700_ref25","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0304-3975(97)00143-6","article-title":"Higher-order rewrite systems and their confluence","volume":"192","author":"Mayr","year":"1998","journal-title":"Theoretical Computer Science"},{"volume-title":"Theory of Categories. Pure and Applied Mathematics: A Series of Monographs and Textbooks","year":"1965","author":"Mitchell","key":"2025121107432355700_ref26"},{"key":"2025121107432355700_ref27","doi-asserted-by":"crossref","DOI":"10.1090\/conm\/092\/1003210","article-title":"Linear logic, $\\ast $-autonomous categories and cofree coalgebras","volume-title":"Categories in Computer Science and Logic","author":"Seely","year":"1989"},{"key":"2025121107432355700_ref28","doi-asserted-by":"crossref","first-page":"198","DOI":"10.2307\/2271658","article-title":"Intensional interpretations of functionals of finite type I","volume":"32","author":"Tait","year":"1967","journal-title":"The Journal of Symbolic Logic"},{"key":"2025121107432355700_ref29","doi-asserted-by":"crossref","first-page":"1029","DOI":"10.1017\/S0960129509990089","article-title":"The algebraic lambda calculus","volume":"19","author":"Vaux","year":"2009","journal-title":"Mathematical Structures in Computer Science"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/35\/8\/exaf053\/65243272\/exaf053.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/35\/8\/exaf053\/65243272\/exaf053.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,11]],"date-time":"2025-12-11T12:43:39Z","timestamp":1765457019000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/doi\/10.1093\/logcom\/exaf053\/8316993"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,4]]},"references-count":29,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2025,11,4]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exaf053","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"type":"print","value":"0955-792X"},{"type":"electronic","value":"1465-363X"}],"subject":[],"published-other":{"date-parts":[[2025,12]]},"published":{"date-parts":[[2025,11,4]]},"article-number":"exaf053"}}