{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,6]],"date-time":"2026-10-06T18:26:15Z","timestamp":1791311175735,"version":"4.3.1"},"reference-count":21,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2009,8,1]],"date-time":"2009-08-01T00:00:00Z","timestamp":1249084800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2009,8]]},"abstract":"<jats:p>\n            We show that context semantics can be fruitfully applied to the quantitative analysis of proof normalization in linear logic. In particular, context semantics lets us define the\n            <jats:italic>weight<\/jats:italic>\n            of a proof-net as a measure of its inherent complexity: it is both an upper bound to normalization time (modulo a polynomial overhead, independently on the reduction strategy) and a lower bound to the amount of resources needed to compute the normal form. Weights are then exploited in proving strong soundness theorems for various subsystems of linear logic, namely elementary linear logic, soft linear logic, and light linear logic.\n          <\/jats:p>","DOI":"10.1145\/1555746.1555749","type":"journal-article","created":{"date-parts":[[2009,8,11]],"date-time":"2009-08-11T13:29:23Z","timestamp":1249997363000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Context semantics, linear logic, and computational complexity"],"prefix":"10.1145","volume":"10","author":[{"given":"Ugo Dal","family":"Lago","sequence":"first","affiliation":[{"name":"Universit\u00e0 di Bologna, Bologna, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2009,8,14]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Asperti A. and Guerrini S. 1998. The Optimal Implementation of Functional Programming Languages. Cambridge University Press.   Asperti A. and Guerrini S. 1998. The Optimal Implementation of Functional Programming Languages. Cambridge University Press."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/504077.504081"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.27"},{"key":"e_1_2_1_4_1","first-page":"1","article-title":"Elementary complexity and geometry of interaction","volume":"45","author":"Baillot P.","year":"2001","journal-title":"Fundamenta Informaticae"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.52"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.21"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00010-5"},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Danos V. and Regnier L. 1995. Proof-nets and Hilbert space. In Advances in Linear Logic J.-Y. Girard Y. Lafont and L. Regnier Eds. Cambridge University Press 307--328.   Danos V. and Regnier L. 1995. Proof-nets and Hilbert space. In Advances in Linear Logic J.-Y. Girard Y. Lafont and L. Regnier Eds. Cambridge University Press 307--328.","DOI":"10.1017\/CBO9780511629150.016"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00049-3"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/646125.680751"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70271-4"},{"key":"e_1_2_1_12_1","volume-title":"Proof-nets: The parallel syntax for proof-theory","author":"Girard J.-Y.","year":"1995"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2700"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90386-T"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143172"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1992.185535"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.10.018"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199483"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/1754621.1754653"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932498"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/1018438.1021853"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1555746.1555749","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1555746.1555749","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:29:31Z","timestamp":1750253371000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1555746.1555749"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,8]]},"references-count":21,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2009,8]]}},"alternative-id":["10.1145\/1555746.1555749"],"URL":"https:\/\/doi.org\/10.1145\/1555746.1555749","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,8]]},"assertion":[{"value":"2006-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2007-10-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-08-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}