{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T05:00:14Z","timestamp":1725512414852},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540797081"},{"type":"electronic","value":"9783540797098"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-79709-8_16","type":"book-chapter","created":{"date-parts":[[2008,5,13]],"date-time":"2008-05-13T14:33:17Z","timestamp":1210689197000},"page":"134-145","source":"Crossref","is-referenced-by-count":0,"title":["A Semantic Proof of Polytime Soundness of Light Affine Logic"],"prefix":"10.1007","author":[{"given":"Ugo Dal","family":"Lago","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Hofmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"Amadio, R.M.: Max-plus quasi-interpretations. In: Proceedings of the 7th International Conference on Typed Lambda Calculi and Applications, pp. 31\u201345 (2003)","key":"16_CR1","DOI":"10.1007\/3-540-44904-3_3"},{"issue":"1","key":"16_CR2","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1145\/504077.504081","volume":"3","author":"A. Asperti","year":"2002","unstructured":"Asperti, A., Roversi, L.: Intuitionistic light affine logic. ACM Transactions on Computational Logic\u00a03(1), 137\u2013175 (2002)","journal-title":"ACM Transactions on Computational Logic"},{"key":"16_CR3","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/S0168-0072(00)00006-3","volume":"104","author":"S. Bellantoni","year":"2000","unstructured":"Bellantoni, S., Niggl, K.H., Schwichtenberg, H.: Higher type recursion, ramification and polynomial time. Annals of Pure and Applied Logic\u00a0104, 17\u201330 (2000)","journal-title":"Annals of Pure and Applied Logic"},{"issue":"2","key":"16_CR4","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/0168-0072(93)90044-E","volume":"63","author":"S. Cook","year":"1993","unstructured":"Cook, S., Urquhart, A.: Functional interpretations of feasible constructive arithmetic. Annals of Pure and Applied Logic\u00a063(2), 103\u2013200 (1993)","journal-title":"Annals of Pure and Applied Logic"},{"doi-asserted-by":"crossref","unstructured":"Coppola, P., Martini, S.: Typing lambda terms in elementary logic with linear constraints. In: Proceedings of the 6th International Conference on Typed Lambda-Calculus and Applications, pp. 76\u201390 (2001)","key":"16_CR5","DOI":"10.1007\/3-540-45413-6_10"},{"key":"16_CR6","first-page":"279","volume":"3","author":"J. Crossley","year":"1994","unstructured":"Crossley, J., Mathai, G., Seely, R.: A logical calculus for polynomial-time realizability. Journal of Methods of Logic in Computer Science\u00a03, 279\u2013298 (1994)","journal-title":"Journal of Methods of Logic in Computer Science"},{"doi-asserted-by":"crossref","unstructured":"Lago, U.D., Hofmann, M.: Quantitative models and implicit complexity. In: Proc. Foundations of Software Technology and Theoretical Computer Science, pp. 189\u2013200 (2005)","key":"16_CR7","DOI":"10.1007\/11590156_15"},{"issue":"2","key":"16_CR8","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1006\/inco.1998.2700","volume":"143","author":"J.-Y. Girard","year":"1998","unstructured":"Girard, J.-Y.: Light linear logic. Information and Computation\u00a0143(2), 175\u2013204 (1998)","journal-title":"Information and Computation"},{"doi-asserted-by":"crossref","unstructured":"Hofmann, M.: Linear types and non-size-increasing polynomial time computation. In: Proceedings of the 14th IEEE Syposium on Logic in Computer Science, pp. 464\u2013473 (1999)","key":"16_CR9","DOI":"10.1109\/LICS.1999.782641"},{"key":"16_CR10","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/S0168-0072(00)00010-5","volume":"104","author":"M. Hofmann","year":"2000","unstructured":"Hofmann, M.: Safe recursion with higher types and BCK-algebra. Annals of Pure and Applied Logic\u00a0104, 113\u2013166 (2000)","journal-title":"Annals of Pure and Applied Logic"},{"issue":"1-2","key":"16_CR11","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/j.tcs.2003.10.019","volume":"318","author":"M. Hofmann","year":"2004","unstructured":"Hofmann, M., Scott, P.: Realizability models for BLL-like languages. Theoretical Computer Science\u00a0318(1-2), 121\u2013137 (2004)","journal-title":"Theoretical Computer Science"},{"key":"16_CR12","first-page":"101","volume-title":"Constructiviey in Mathematics","author":"G. Kreisel","year":"1959","unstructured":"Kreisel, G.: Interpretation of analysis by means of constructive functions of finite types. In: Heyting, A. (ed.) Constructiviey in Mathematics, pp. 101\u2013128. North-Holland, Amsterdam (1959)"},{"key":"16_CR13","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1016\/j.tcs.2003.10.018","volume":"318","author":"Y. Lafont","year":"2004","unstructured":"Lafont, Y.: Soft linear logic and polynomial time. Theoretical Computer Science\u00a0318, 163\u2013180 (2004)","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"16_CR14","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1016\/j.tcs.2004.02.037","volume":"318","author":"U.D. Lago","year":"2004","unstructured":"Lago, U.D., Martini, S.: Phase semantics and decidability of elementary affine logic. Theor. Comput. Sci.\u00a0318(3), 409\u2013433 (2004)","journal-title":"Theor. Comput. Sci."},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/3-540-44622-2_29","volume-title":"Computer Science Logic","author":"A.S. Murawski","year":"2000","unstructured":"Murawski, A.S., Luke Ong, C.-H.: Discreet games, light affine logic and ptime computation. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. LNCS, vol.\u00a01862, pp. 427\u2013441. Springer, Heidelberg (2000)"},{"key":"16_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/3-540-48168-0_33","volume-title":"Computer Science Logic","author":"L. Roversi","year":"1999","unstructured":"Roversi, L.: A p-time completeness proof for light logics. In: Flum, J., Rodr\u00edguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol.\u00a01683, pp. 469\u2013483. Springer, Heidelberg (1999)"}],"container-title":["Lecture Notes in Computer Science","Computer Science \u2013 Theory and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-79709-8_16.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:28:44Z","timestamp":1619522924000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-79709-8_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540797081","9783540797098"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-79709-8_16","relation":{},"subject":[]}}