{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:35:38Z","timestamp":1725489338398},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540442400"},{"type":"electronic","value":"9783540457930"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45793-3_11","type":"book-chapter","created":{"date-parts":[[2007,8,16]],"date-time":"2007-08-16T12:03:26Z","timestamp":1187265806000},"page":"151-166","source":"Crossref","is-referenced-by-count":2,"title":["Proofnets and Context Semantics for the Additives"],"prefix":"10.1007","author":[{"given":"Harry G.","family":"Mairson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xavier","family":"Rival","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,9,2]]},"reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"S. Abramsky and P.-A. Melli\u00e8s. Concurrent games and full completeness. In LICS\u201999, pages 431\u2013442. IEEE, July 1999.","DOI":"10.1109\/LICS.1999.782638"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Samson Abramsky and Guy McCusker. Linearity, sharing and state: a fully abstract game semantics for Idealized Algol with active expressions (extended abstract). In Proceedings of 1996 Workshop on Linear Logic, volume 3 of Electronic notes in Theoretical Computer Science. Elsevier, 1996.","DOI":"10.1016\/S1571-0661(05)80398-6"},{"issue":"1","key":"11_CR3","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1016\/0304-3975(94)00104-9","volume":"135","author":"G. Bellin","year":"1994","unstructured":"G. Bellin and P. J. Scott. On the \u03c0-calculus and linear logic. Theoretical Computer Science, 135(1):11\u201365, December 1994.","journal-title":"Theoretical Computer Science"},{"key":"11_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.-Y. Girard","year":"1987","unstructured":"Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1\u2013102, 1987.","journal-title":"Theoretical Computer Science"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Jean-Yves Girard. Geometry of interaction I: Interpretation of system F. In Logic Colloquium\u2019 88, pages 221\u2013260. North-Holland, 1989.","DOI":"10.1016\/S0049-237X(08)70271-4"},{"key":"11_CR6","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1017\/CBO9780511629150.017","volume-title":"Advances in Linear Logic","author":"J.-Y. Girard","year":"1995","unstructured":"Jean-Yves Girard. Geometry of interaction III: The general case. In Advances in Linear Logic, pages 329\u2013389. Cambridge University Press, 1995. Proceedings of the 1993 Workshop on Linear Logic, Cornell Univesity, Ithaca."},{"key":"11_CR7","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1017\/CBO9780511629150","volume-title":"Advances in Linear Logic","author":"J.-Y. Girard","year":"1995","unstructured":"Jean-Yves Girard. Linear logic: its syntax and semantics. In Advances in Linear Logic, pages 1\u201342. Cambridge University Press, 1995. Proceedings of the 1993 Workshop on Linear Logic, Cornell Univesity, Ithaca."},{"key":"11_CR8","unstructured":"Jean-Yves Girard. Proof-nets: The parallel syntax for proof-theory. In Logic and Algebra. Marcel Dekker, 1996."},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"Georges Gonthier, Mart\u00edn Abadi, and Jean-Jacques L\u00e9vy. The geometry of optmnal lambda reduction. In POPL\u201992, pages 15\u201326, Albuquerque, January 1992. ACM Press.","DOI":"10.1145\/143165.143172"},{"key":"11_CR10","first-page":"223","volume-title":"LICS\u201992","author":"G. Gonthier","year":"1992","unstructured":"Georges Gonthier, Mart\u00edn Abadi, and Jean-Jacques L\u00e9vy. Linear logic without boxes. In LICS\u201992, pages 223\u201334. IEEE, Los Alamitos, 1992."},{"key":"11_CR11","first-page":"47","volume-title":"POPL\u201990","author":"T. G. Griffin","year":"1990","unstructured":"Timothy G. Griffin. The formulae-as-types notion of control. In POPL\u201990, pages 47\u201357. ACM Press, New York, 1990."},{"key":"11_CR12","volume-title":"Communicating Sequential Processes","author":"C. A. R. Hoare","year":"1985","unstructured":"C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs, NJ, 1985. & 0-13-153289-8."},{"key":"11_CR13","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1017\/CBO9780511629150.012","volume-title":"Advances in Linear Logic","author":"Y. Lafont","year":"1995","unstructured":"Y. Lafont. From proof nets to interaction nets. In Advances in Linear Logic, pages 225\u2013247. Cambridge University Press, 1995. Proceedings of the 1993 Workshop on Linear Logic, Cornell Univesity, Ithaca."},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"John Lamping. An algorithm for optimal lambda-calculus reductions. In POPL\u201990, pages 16\u201330. ACM Press, January 1990.","DOI":"10.1145\/96709.96711"},{"key":"11_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1007\/3-540-45413-6_23","volume-title":"TLCA\u201901","author":"O. Laurent","year":"2001","unstructured":"Olivier Laurent. A token machine for full geometry of interaction (extended abstract). In TLCA\u201901, volume 2044, pages 283\u2013297. LNCS, Springer-Verlag, May 2001."},{"key":"11_CR16","series-title":"Lect Notes Comput Sci","volume-title":"ESOP\u20192000","author":"J. L. Lawall","year":"2000","unstructured":"Julia L. Lawall and Harry G. Mairson. Sharing continuations: proofnets for languages with explicit control. In ESOP\u20192000, volume 1782. LNCS, Springer-Verlag, 2000."},{"key":"11_CR17","unstructured":"Robin Milner. Communicating and Mobile Systems: the \u03c0-Calculus. Cambridge University Press, May 1999."},{"key":"11_CR18","unstructured":"Chetan R. Murthy. Extracting constructive content from classical proofs. Technical Report TR90-1151, Cornell University, Computer Science Department, August 1990."},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Lorenzo Tortora de Falco. The additive multiboxes. Annals of Pure and Applied Logic. To appear.","DOI":"10.1016\/S0168-0072(02)00042-8"},{"key":"11_CR20","unstructured":"Lorenzo Tortora de Falco. Additives of linear logic and normalization-part 1: a (restricted) church-rosser property. Theoretical Computer Science."}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45793-3_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,2]],"date-time":"2019-05-02T04:34:25Z","timestamp":1556771665000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45793-3_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540442400","9783540457930"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-45793-3_11","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}