{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T22:54:23Z","timestamp":1672613663406},"reference-count":28,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2001,2,1]],"date-time":"2001-02-01T00:00:00Z","timestamp":980985600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":4549,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2001,2]]},"DOI":"10.1016\/s0304-3975(00)00094-3","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T17:01:59Z","timestamp":1027616519000},"page":"185-237","source":"Crossref","is-referenced-by-count":7,"title":["Proof nets, garbage, and computations"],"prefix":"10.1016","volume":"253","author":[{"given":"Stefano","family":"Guerrini","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Simone","family":"Martini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrea","family":"Masini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"issue":"1\u20132","key":"10.1016\/S0304-3975(00)00094-3_BIB1","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(93)90181-R","article-title":"Computational interpretations of linear logic","volume":"111","author":"Abramsky","year":"1993","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(00)00094-3_BIB2","doi-asserted-by":"crossref","first-page":"3","DOI":"10.3233\/FI-1995-22121","article-title":"Linear logic, comonads and optimal reductions","volume":"22","author":"Asperti","year":"1995","journal-title":"Fund. Inform."},{"key":"10.1016\/S0304-3975(00)00094-3_BIB3","doi-asserted-by":"crossref","unstructured":"A. Asperti, V. Danos, C. Laneve L. Regnier, Paths in the lambda-calculus: three years of communications without understanding, Proc. 9th Ann. Symp. on Logic in Computer Science, Paris, France, July 1994, pp. 426\u2013436.","DOI":"10.1109\/LICS.1994.316048"},{"key":"10.1016\/S0304-3975(00)00094-3_BIB4","unstructured":"A. Asperti, S. Guerrini, The Optimal Implementation of Functional Programming Languages, Cambridge Tracts in Theoretical Computer Science, Vol. 45, Cambridge University Press, Cambridge, 1998."},{"issue":"2","key":"10.1016\/S0304-3975(00)00094-3_BIB5","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1016\/0304-3975(95)00062-3","article-title":"Interaction Systems II","volume":"159","author":"Asperti","year":"1996","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(00)00094-3_BIB6","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1016\/0168-0072(94)00033-Y","article-title":"Sequent reconstruction in LLM \u2013 a sweepline proof","volume":"73","author":"Banach","year":"1995","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S0304-3975(00)00094-3_BIB7","doi-asserted-by":"crossref","unstructured":"G. Gonthier, M. Abadi, J.J. L\u00e9vy, The geometry of optimal lambda reduction, Proc. 19th Annu. ACM Symp. on Principles of Programming Languages, Albuquerque, NM, January 1992, pp. 15\u201326.","DOI":"10.1145\/143165.143172"},{"key":"10.1016\/S0304-3975(00)00094-3_BIB8","doi-asserted-by":"crossref","unstructured":"G. Gonthier, M. Abadi, J.-J. L\u00e9vy, Linear logic without boxes, Proc. 7th Annu. Symp. on Logic in Computer Science, Santa Cruz, CA, June 1992, pp. 223\u2013234.","DOI":"10.1109\/LICS.1992.185535"},{"issue":"1","key":"10.1016\/S0304-3975(00)00094-3_BIB9","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":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(00)00094-3_BIB10","unstructured":"S. Guerrini, Theoretical and practical issues of optimal implementations of functional languages, Ph.D. Thesis, Dipartimento di Informatica, Pisa, 1996, TD-3\/96."},{"key":"10.1016\/S0304-3975(00)00094-3_BIB11","doi-asserted-by":"crossref","unstructured":"S. Guerrini, Correctness of multiplicative proof nets is linear, Proc. 14th Ann. Symp. on Logic in Computer Science LICS 99, Tiento, Italy, July 1999, pp. 454\u2013463.","DOI":"10.1109\/LICS.1999.782640"},{"key":"10.1016\/S0304-3975(00)00094-3_BIB12","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1016\/S0304-3975(99)00050-X","article-title":"A general theory of sharing graphs","volume":"227","author":"Guerrini","year":"1999","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(00)00094-3_BIB13","unstructured":"S. Guerrini, A. Masini, Parsing MELL proof nets, Theoret. Comput. Sci. (1999), to appear."},{"key":"10.1016\/S0304-3975(00)00094-3_BIB14","doi-asserted-by":"crossref","unstructured":"S. Guerrini, S. Martini, A. Masini, Coherence for sharing proof nets, in: H. Ganzinger (Ed.), Proc. 7th Internat. Conf. on Rewriting Techniques and Applications (RTA-96), Lecture Notes in Computer Science, Vol. 1103, New Brunswick, NJ, USA, Springer, Berlin, 1996, pp. 215\u2013229 (extended abstract).","DOI":"10.1007\/3-540-61464-8_54"},{"key":"10.1016\/S0304-3975(00)00094-3_BIB15","series-title":"Typed Lambda Calculi and Applications","article-title":"Proof nets, garbage, and computations","volume":"Vol. 1210","author":"Guerrini","year":"1997"},{"key":"10.1016\/S0304-3975(00)00094-3_BIB16","doi-asserted-by":"crossref","unstructured":"Y. Lafont, Interaction nets, in: Proc. 17th Annu. ACM Symp. on Principles of Programming Languages, San Francisco, CA, January 1990, pp. 95\u2013108.","DOI":"10.1145\/96709.96718"},{"key":"10.1016\/S0304-3975(00)00094-3_BIB17","doi-asserted-by":"crossref","unstructured":"J. Lamping, An algorithm for optimal lambda calculus reduction, in: Proc. 17th Annu. ACM Symp. on Principles of Programming Languages, San Francisco, CA, January 1990, pp. 16\u201330.","DOI":"10.1145\/96709.96711"},{"key":"10.1016\/S0304-3975(00)00094-3_BIB18","doi-asserted-by":"crossref","unstructured":"J.L. Lawall, H.G. Mairson, Optimality and inefficiency: what isn't a cost model of the lambda calculus? Proc. 1996 ACM SIGPLAN Internat. Conf. on Functional Programming, Philadelphia, Pennsylvania, 24\u201326 May 1996, pp. 92\u2013101.","DOI":"10.1145\/232627.232639"},{"key":"10.1016\/S0304-3975(00)00094-3_BIB19","unstructured":"J.-J. L\u00e9vy, R\u00e9ductions correctes et optimales dans le lambda-calcul, Ph.D. Thesis, Universit\u00e9 Paris VII, 1978."},{"key":"10.1016\/S0304-3975(00)00094-3_BIB20","series-title":"To H.B. Curry","first-page":"159","article-title":"Optimal Reductions in the lambda-calculus","author":"L\u00e9vy","year":"1980"},{"key":"10.1016\/S0304-3975(00)00094-3_BIB21","unstructured":"J. Maraist, Separating weakening and contraction in a linear lambda calculus, Technical Report iratr-1996-25, Universit\u00e4t Karlsruhe, Institut f\u00fcr Programmstrukturen und Datenorganisation, 1996."},{"key":"10.1016\/S0304-3975(00)00094-3_BIB22","doi-asserted-by":"crossref","unstructured":"S. Martini, a. Masini, On the fine structure of the exponential rule, in: J.-Y. Girard, Y. Lafont, L. Regnier (Eds.), Advances in Linear Logic, Cambridge University Press, Cambridge, 1995, pp. 197\u2013210, Proceedings of the Workshop on Linear Logic, Ithaca, New York, June 1993.","DOI":"10.1017\/CBO9780511629150.010"},{"key":"10.1016\/S0304-3975(00)00094-3_BIB23","doi-asserted-by":"crossref","unstructured":"J. Maraist, M. Odersky, D.N. Turner, P. Wadler, Call-by-name, call-by-value, call-by-need and the linear lambda calculus, Theoret. Comput. Sci., 1999, to appear.","DOI":"10.1016\/S0304-3975(98)00358-2"},{"key":"10.1016\/S0304-3975(00)00094-3_BIB24","first-page":"26","article-title":"Pi-nets","volume":"Vol. 788","author":"Milner","year":"1994"},{"issue":"1","key":"10.1016\/S0304-3975(00)00094-3_BIB25","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","article-title":"A calculus of mobile processes, I","volume":"100","author":"Milner","year":"1992","journal-title":"Inform. Comput."},{"issue":"1","key":"10.1016\/S0304-3975(00)00094-3_BIB26","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1016\/0890-5401(92)90009-5","article-title":"A calculus of mobile processes, II","volume":"100","author":"Milner","year":"1992","journal-title":"Inform. Comput."},{"key":"10.1016\/S0304-3975(00)00094-3_BIB27","series-title":"The Implementation of Functional Programming Languages","author":"Peyton Jones","year":"1987"},{"key":"10.1016\/S0304-3975(00)00094-3_BIB28","unstructured":"L. Regnier, Lambda-Calcul et Reseaux, Ph.D. Thesis, Universit\u00e9 Paris 7, January 1992."}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397500000943?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397500000943?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,1,17]],"date-time":"2020-01-17T07:31:33Z","timestamp":1579246293000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397500000943"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,2]]},"references-count":28,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2001,2]]}},"alternative-id":["S0304397500000943"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(00)00094-3","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2001,2]]}}}