{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:21:41Z","timestamp":1751660501223},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540419600"},{"type":"electronic","value":"9783540454137"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45413-6_10","type":"book-chapter","created":{"date-parts":[[2007,8,4]],"date-time":"2007-08-04T08:51:43Z","timestamp":1186217503000},"page":"76-90","source":"Crossref","is-referenced-by-count":15,"title":["Typing Lambda Terms in Elementary Logic with Linear Constraints"],"prefix":"10.1007","author":[{"given":"Paolo","family":"Coppola","sequence":"first","affiliation":[]},{"given":"Simone","family":"Martini","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,4,25]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Andrea Asperti. Light affine logic. In Proc. of the 13-th Annual IEEE Symposium on Logic in Computer Science (LICS\u2019 98), pages 300\u2013308, Indianapolis, U.S.A., 1998.","DOI":"10.1109\/LICS.1998.705666"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Andrea Asperti, Paolo Coppola, and Simone Martini. (Optimal) duplication is not elementary recursive. In ACM POPL\u201900, pages 96\u2013107, Boston, Massachusetts, January 19\u201321, 2000.","DOI":"10.1145\/325694.325707"},{"key":"10_CR3","unstructured":"Andrea Asperti and Stefano Guerrini. The Optimal Implementation of Functional Programming Languages, volume 45 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1998."},{"key":"10_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/BFb0037099","volume-title":"TLCA\u201993","author":"N. Benton","year":"1993","unstructured":"Nick Benton, Gavin Bierman, Valeria de Paiva, and Martin Hyland. A term calculus for intuitionistic linear logic. TLCA\u201993, volume 664 of Lecture Notes in Computer Science, pages 75\u201390, March 1993."},{"key":"10_CR5","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/BF02390456","volume":"33","author":"V. Danos","year":"1995","unstructured":"Vincent Danos, Jean-Baptiste Joinet and Harold Schellinx. On the linear decoration of intuitionistic derivations. Archive for Mathematical Logic, 33:387\u2013412, 1995.","journal-title":"Archive for Mathematical Logic"},{"key":"10_CR6","first-page":"143","volume":"204","author":"J.-Y. Girard","year":"1998","unstructured":"Jean-Yves Girard. Light linear logic. Information and Computation, 204:143\u2013175, 1998.","journal-title":"Information and Computation"},{"key":"10_CR7","unstructured":"Vinod K. Kathail. Optimal Interpreters for Lambda-calculus Based Functional Programming Languages. PhD thesis, MIT, May 1990."},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"John Lamping. An Algorithm for Optimal Lambda Calculus Reduction. In ACM POPL\u2019 90, pages 16\u201330, New York, NY, USA, 1990.","DOI":"10.1145\/96709.96711"},{"key":"10_CR9","first-page":"159","volume-title":"H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"J.-J. L\u00e9vy","year":"1980","unstructured":"Jean-Jacques L\u00e9vy. Optimal reductions in the lambda-calculus. In Jonathan P. Seldin and J. Roger Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 159\u2013191. Academic Press, London, 1980."},{"issue":"2","key":"10_CR10","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1016\/0304-3975(92)90020-G","volume":"103","author":"H. G. Mairson","year":"1992","unstructured":"Harry G. Mairson. A simple proof of a theorem of Statman. Theoretical Computer Science, 103(2):387\u2013394, September 1992.","journal-title":"Theoretical Computer Science"},{"key":"10_CR11","unstructured":"Alberto Pravato and Luca Roversi. \u039b! considered both as a paradigmatic language and a meta-language. In Fifth Italian Conference on Theoretical Computer Science, Salerno (Italy), 1995."},{"key":"10_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1007\/3-540-49366-2_4","volume-title":"Proc. of the Asian Computing Science Conference (ASIAN\u201998)","author":"L. Roversi","year":"1998","unstructured":"Luca Roversi. A Polymorphic Language which Is Typable and Poly-step. In Proc. of the Asian Computing Science Conference (ASIAN\u201998), volume 1538 of Lecture Notes in Computer Science, pages 43\u201360, Manila (The Philippines), 1998."},{"key":"10_CR13","unstructured":"Harold Schellinx. The Noble Art of Linear Decorating. PhD thesis, Institute for Logic, Language and Computation, University of Amsterdam, 1994."}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45413-6_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T19:06:41Z","timestamp":1556737601000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45413-6_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540419600","9783540454137"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-45413-6_10","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}