{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T06:54:26Z","timestamp":1760079266221},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540679011"},{"type":"electronic","value":"9783540446125"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44612-5_62","type":"book-chapter","created":{"date-parts":[[2007,5,5]],"date-time":"2007-05-05T13:28:20Z","timestamp":1178371700000},"page":"670-679","source":"Crossref","is-referenced-by-count":13,"title":["Abstract Syntax and Variable Binding for Linear Binders"],"prefix":"10.1007","author":[{"given":"Miki","family":"Tanaka","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,6,1]]},"reference":[{"key":"62_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"78","DOI":"10.1007\/BFb0028008","volume-title":"Computer Science Logic\u2019 97 Selected Papers","author":"A. Barber","year":"1998","unstructured":"A. Barber, P. Gardner, M. Hasegawa, and G. Plotkin. From action calculi and linear logic. In Computer Science Logic\u2019 97 Selected Papers, volume 1414 of Lecture Notes in Computer Science, pages 78\u201397, 1998."},{"key":"62_CR2","doi-asserted-by":"crossref","unstructured":"F. Bergeron, G. Labelle, and P. Leroux. Combinatorial species and tree-like structures, volume 67 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1998.","DOI":"10.1017\/CBO9781107325913"},{"key":"62_CR3","unstructured":"A. Barber, G. Plotkin. Dual intuitionistic linear logic. Submitted."},{"key":"62_CR4","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N. Bruijn de","year":"1972","unstructured":"N. de Bruijn. Lambda calculus notations with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae, 34:381\u2013391, 1972.","journal-title":"Indagationes Mathematicae"},{"key":"62_CR5","doi-asserted-by":"crossref","unstructured":"B.J. Day. On closed categories of functors. In Midwest Category Seminar Reports IV, volume 137 of Lecture Notes in Mathematics, pages 1\u201338, 1970.","DOI":"10.1007\/BFb0060438"},{"key":"62_CR6","doi-asserted-by":"crossref","unstructured":"M. Fiore, G. Plotkin, and D. Turi. Abstract syntax and variable binding. In Proceedings of 14th Symposium on Logic in Computer Science, pages 193\u2013202, IEEE Computer Society Press, 1999.","DOI":"10.1109\/LICS.1999.782615"},{"key":"62_CR7","doi-asserted-by":"crossref","unstructured":"M. Fiore, G. Plotkin. An axiomatisation of computationally adequate domain theoretic model of FPC. In Proceedings of 9th Symposium on Logic in Computer Science, pages 92\u2013102, IEEE Computer Society Press, 1994.","DOI":"10.1109\/LICS.1994.316083"},{"key":"62_CR8","doi-asserted-by":"crossref","unstructured":"M. Gabbay, A. Pitts. A new approach to abstract syntax involving binders. In Proceedings of 14th Symposium on Logic in Computer Science, pages 214\u2013224, IEEE Computer Society Press, 1999.","DOI":"10.1109\/LICS.1999.782617"},{"key":"62_CR9","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1016\/S0022-4049(97)00070-4","volume":"120","author":"R. Gordon","year":"1997","unstructured":"R. Gordon, J.A. Power. Enrichment through variation. Journal of Pure and Applied Algebra, 120:167\u2013185, 1997.","journal-title":"Journal of Pure and Applied Algebra"},{"key":"62_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/3-540-48959-2_15","volume-title":"Typed Lambda Calculi and its Applications","author":"M. Hasegawa","year":"1999","unstructured":"M. Hasegawa. Logical predicates for intuitionistic linear type theories. In Typed Lambda Calculi and its Applications, volume 1581 of Lecture Notes in Computer Science, pages 198\u2013212, 1999."},{"key":"62_CR11","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/0022-4049(86)90005-8","volume":"43","author":"G.B. Im","year":"1986","unstructured":"G.B. Im, G.M. Kelly. A universal property of the convolution monoidal structure. J. of Pure and Applied Algebra, 43:75\u201388, 1986.","journal-title":"J. of Pure and Applied Algebra"},{"key":"62_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0001-8708(81)90052-9","volume":"42","author":"A. Joyal","year":"1981","unstructured":"A. Joyal. Une th\u00e9orie combinatoire des s\u00e9ries formelles. Advances in Mathematics, 42:1\u201382, 1981.","journal-title":"Advances in Mathematics"},{"key":"62_CR13","doi-asserted-by":"crossref","unstructured":"A. Joyal. Foncteurs analytiques et esp\u00e9ces de structures. In Combinatoire enumerative, volume 1234 of Lecture Notes in Mathematics, pages 126\u2013159, Springer-Verlag, 1987.","DOI":"10.1007\/BFb0072514"},{"key":"62_CR14","unstructured":"J. McCarthy. Towards a mathematical science of computation. In IFIP Congress 1962, North-Holland, 1963."},{"key":"62_CR15","doi-asserted-by":"crossref","unstructured":"E. Moggi. Computational lambda-calculus and monads. In Proceedings of 4th Symposium on Logic in Computer Science, pages 14\u201323, IEEE Computer Society Press, 1989.","DOI":"10.1109\/LICS.1989.39155"},{"key":"62_CR16","doi-asserted-by":"crossref","unstructured":"P.W. O\u2019Hearn, J.C. Reynolds. From Algol to polymorphic linear lambda-calculus. Journal of the ACM, January 2000, Vol. 47 No. 1.","DOI":"10.1145\/331605.331611"},{"key":"62_CR17","doi-asserted-by":"crossref","unstructured":"P. W. O\u2019Hearn, R. D. Tennent. ed. Algol-like languages, In Progress in Theoretical Computer Science, Birkhauser, 1997.","DOI":"10.1007\/978-1-4757-3851-3"},{"key":"62_CR18","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1017\/S0960129500000311","volume":"3","author":"P. W. O\u2019Hearn","year":"1993","unstructured":"P. W. O\u2019Hearn. A model for Syntactic Control of Interference. Mathematical Structures in Computer Science, 3:435\u2013465, 1993.","journal-title":"Mathematical Structures in Computer Science"},{"key":"62_CR19","first-page":"222","volume-title":"Proceedings of the International Computing Symposium","author":"C. Strachey","year":"1972","unstructured":"C. Strachey. The varieties of programming language. In Proceedings of the International Computing Symposium, pages 222\u2013233. Cini Foundation, Venice, 1972."},{"key":"62_CR20","doi-asserted-by":"crossref","unstructured":"M. Tanaka. Abstract syntax and variable binding for linear binders (extended version). Draft, 2000.","DOI":"10.1007\/3-540-44612-5_62"},{"key":"62_CR21","doi-asserted-by":"crossref","unstructured":"D. Turi, G. Plotkin. Towards a mathematical operational semantics. In Proceedings of 12th Symposium on Logic in Computer Science, pages 280\u2013291, IEEE Computer Society Press, 1997.","DOI":"10.1109\/LICS.1997.614955"}],"container-title":["Lecture Notes in Computer Science","Mathematical Foundations of Computer Science 2000"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44612-5_62","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,21]],"date-time":"2020-04-21T19:15:01Z","timestamp":1587496501000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44612-5_62"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540679011","9783540446125"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-44612-5_62","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}