{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,6,4]],"date-time":"2024-06-04T22:42:22Z","timestamp":1717540942324},"reference-count":39,"publisher":"Cambridge University Press (CUP)","issue":"5","license":[{"start":{"date-parts":[[2014,11,10]],"date-time":"2014-11-10T00:00:00Z","timestamp":1415577600000},"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,6]]},"abstract":"<jats:p>Linearity is a multi-faceted and ubiquitous notion in the analysis and development of programming language concepts. We study linearity in a denotational perspective by picking out programs that correspond to linear functions between domains.<\/jats:p><jats:p>We propose a PCF-like language imposing linear constraints on the use of variable to program only linear functions. To entail a full abstraction result, we introduce some higher-order operators related to exception handling and parallel evaluation. We study several notions of operational equivalence and show them to coincide with our language. Finally, we present a new operational evaluation of the language that provides the base for a real implementation. It exploits the denotational linearity to provide an efficient evaluation semantics SECD-like, that avoids the use of closures.<\/jats:p>","DOI":"10.1017\/s0960129514000401","type":"journal-article","created":{"date-parts":[[2014,11,10]],"date-time":"2014-11-10T17:59:51Z","timestamp":1415642391000},"page":"829-867","source":"Crossref","is-referenced-by-count":2,"title":["On the reification of semantic linearity"],"prefix":"10.1017","volume":"26","author":[{"given":"MARCO","family":"GABOARDI","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"LUCA","family":"PAOLINI","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"MAURO","family":"PICCOLO","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,11,10]]},"reference":[{"key":"S0960129514000401_ref36","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2005.11.002"},{"key":"S0960129514000401_ref20","unstructured":"Gaboardi M. and Paolini L. (2007) Syntactical, operational and denotational linearity. In: Workshop on Linear Logic, Ludics, Implicit Complexity and Operator Algebras. Dedicated to Jean-Yves Girard on his 60th birthday. Certosa di Pontignano, Siena."},{"key":"S0960129514000401_ref5","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.11.014"},{"key":"S0960129514000401_ref14","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1033"},{"key":"S0960129514000401_ref23","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"S0960129514000401_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-15975-4_37"},{"key":"S0960129514000401_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73147-4_9"},{"key":"S0960129514000401_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80398-6"},{"key":"S0960129514000401_ref27","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58027-1_21"},{"key":"S0960129514000401_ref30","unstructured":"Johnsson T. (1987) Compiling Lazy Functional Languages, Ph.D. thesis, Department of Computer Sciences, Chalmers University of Technology, Goteborg, Sweden."},{"key":"S0960129514000401_ref33","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(01)00110-5"},{"key":"S0960129514000401_ref28","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2917"},{"key":"S0960129514000401_ref32","first-page":"32","article-title":"Notions of computability at higher types I","volume":"19","author":"Longley","year":"2000","journal-title":"Lecture Notes in Logic"},{"key":"S0960129514000401_ref19","doi-asserted-by":"crossref","unstructured":"Ehrhard T. (1995) Hypercoherence: A strongly stable model of linear logic. In: Girard J.-Y. , Lafont Y. and Regnier L. (eds.) Proceedings of the Workshop on Advances in Linear Logic. London Mathematical Society Lecture Note Series 222, Cambridge University Press, Ithaca, New York 83\u2013108.","DOI":"10.1017\/CBO9780511629150.005"},{"key":"S0960129514000401_ref17","volume-title":"Computability, Complexity and Languages","author":"Davis","year":"1983"},{"key":"S0960129514000401_ref31","volume-title":"Reflections on Type Theory","author":"Klop","year":"2007"},{"key":"S0960129514000401_ref1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2930"},{"key":"S0960129514000401_ref22","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(86)90044-7"},{"key":"S0960129514000401_ref37","first-page":"97","volume-title":"Proceedings of the 10th International Association for Computing Machinery's Special interest Group on Programming Languages Conference on Principles and Practice of Declarative Programming","author":"Paolini","year":"2008"},{"key":"S0960129514000401_ref34","doi-asserted-by":"publisher","DOI":"10.2178\/bsl\/1140640943"},{"key":"S0960129514000401_ref18","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"S0960129514000401_ref6","unstructured":"Augustsson L. (1987) Compiling Lazy Functional Languages, Part II, Ph.D. thesis, Department of Computer Sciences, Chalmers University of Technology, Goteborg, Sweden."},{"key":"S0960129514000401_ref24","volume-title":"Proofs and Types","author":"Girard","year":"1989"},{"key":"S0960129514000401_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/11874683_8"},{"key":"S0960129514000401_ref25","volume-title":"Semantics of Programming Languages: Structures and Techniques","author":"Gunter","year":"1992"},{"key":"S0960129514000401_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-08860-1_7"},{"key":"S0960129514000401_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(82)80002-9"},{"key":"S0960129514000401_ref12","doi-asserted-by":"crossref","unstructured":"Bucciarelli A. and Ehrhard T. (1991) Sequentiality and strong stability. In: Proceedings of the Symposium on Logic in Computer Science 138\u2013145.","DOI":"10.1109\/LICS.1991.151638"},{"key":"S0960129514000401_ref16","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139171496","volume-title":"Computability: An Introduction to Recursive Function Theory","author":"Cutland","year":"1980"},{"key":"S0960129514000401_ref9","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796899003639"},{"key":"S0960129514000401_ref11","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.22.4"},{"key":"S0960129514000401_ref26","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(89)90100-X"},{"key":"S0960129514000401_ref39","volume-title":"Advanced Topics in Types and Programming Languages","author":"Walker","year":"2005"},{"key":"S0960129514000401_ref13","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90005-E"},{"key":"S0960129514000401_ref38","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"S0960129514000401_ref21","first-page":"372","volume-title":"Proceeding of the 16th Association for Computing Machinery's Special interest Group on Programming Language, International Conference on Functional Programming","author":"Gaboardi","year":"2011"},{"key":"S0960129514000401_ref15","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.011"},{"key":"S0960129514000401_ref10","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80874-0"},{"key":"S0960129514000401_ref35","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1093\/oso\/9780198537809.003.0003","volume-title":"Handbook of Logic in Computer Science","author":"Ong","year":"1995"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129514000401","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,4]],"date-time":"2024-06-04T22:11:34Z","timestamp":1717539094000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129514000401\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,10]]},"references-count":39,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2016,6]]}},"alternative-id":["S0960129514000401"],"URL":"https:\/\/doi.org\/10.1017\/s0960129514000401","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,11,10]]}}}