{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,20]],"date-time":"2026-09-20T10:28:59Z","timestamp":1789900139693,"version":"4.0.1"},"reference-count":21,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2009,4,7]],"date-time":"2009-04-07T00:00:00Z","timestamp":1239062400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory Comput Syst"],"published-print":{"date-parts":[[2010,5]]},"DOI":"10.1007\/s00224-009-9210-x","type":"journal-article","created":{"date-parts":[[2009,4,6]],"date-time":"2009-04-06T17:45:27Z","timestamp":1239039927000},"page":"673-689","source":"Crossref","is-referenced-by-count":7,"title":["A Semantic Proof of Polytime Soundness of\u00a0Light Affine Logic"],"prefix":"10.1007","volume":"46","author":[{"given":"Ugo","family":"Dal Lago","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Martin","family":"Hofmann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2009,4,7]]},"reference":[{"key":"9210_CR1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/3-540-44904-3_3","volume-title":"Proc. of the 7th International Conference on Typed Lambda Calculi and Applications","author":"R.M. Amadio","year":"2003","unstructured":"Amadio, R.M.: Max-plus quasi-interpretations. In: Proc. of the 7th International Conference on Typed Lambda Calculi and Applications. LNCS, vol. 2701, pp. 31\u201345. Springer, Berlin (2003)"},{"issue":"1","key":"9210_CR2","doi-asserted-by":"crossref","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 Trans. Comput. Log. 3(1), 137\u2013175 (2002)","journal-title":"ACM Trans. Comput. Log."},{"key":"9210_CR3","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"The Lambda Calculus: Its Syntax and Semantics","author":"H. Barendregt","year":"1984","unstructured":"Barendregt, H.: The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics. North Holland, Amsterdam (1984)"},{"key":"9210_CR4","doi-asserted-by":"crossref","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. Ann. Pure Appl. Logic 104, 17\u201330 (2000)","journal-title":"Ann. Pure Appl. Logic"},{"issue":"2","key":"9210_CR5","doi-asserted-by":"crossref","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. Ann. Pure Appl. Logic 63(2), 103\u2013200 (1993)","journal-title":"Ann. Pure Appl. Logic"},{"key":"9210_CR6","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1007\/3-540-45413-6_10","volume-title":"Proc. of the 6th International Conference on Typed Lambda Calculi and Applications","author":"P. Coppola","year":"2001","unstructured":"Coppola, P., Martini, S.: Typing lambda terms in elementary logic with linear constraints. In: Proc. of the 6th International Conference on Typed Lambda Calculi and Applications. LNCS, vol. 2044, pp. 76\u201390. Springer, Berlin (2001)"},{"key":"9210_CR7","first-page":"279","volume":"3","author":"J. Crossley","year":"1994","unstructured":"Crossley, J., Mathai, G., Seely, R.: A logical calculus for polynomial-time realizability. J. Methods Logic Comput. Sci. 3, 279\u2013298 (1994)","journal-title":"J. Methods Logic Comput. Sci."},{"key":"9210_CR8","series-title":"LNCS","first-page":"189","volume-title":"Proc. Foundations of Software Technology and Theoretical Computer Science","author":"U. Dal Lago","year":"2005","unstructured":"Dal Lago, U., Hofmann, M.: Quantitative models and implicit complexity. In: Proc. Foundations of Software Technology and Theoretical Computer Science. LNCS, vol. 3821, pp. 189\u2013200. Springer, Berlin (2005)"},{"issue":"3","key":"9210_CR9","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1016\/j.tcs.2004.02.037","volume":"318","author":"U. Dal Lago","year":"2004","unstructured":"Dal Lago, U., Martini, S.: Phase semantics and decidability of elementary affine logic. Theor. Comput. Sci. 318(3), 409\u2013433 (2004)","journal-title":"Theor. Comput. Sci."},{"issue":"1\u20133","key":"9210_CR10","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1016\/j.tcs.2008.01.044","volume":"398","author":"U. Dal Lago","year":"2008","unstructured":"Dal Lago, U., Martini, S.: The weak lambda calculus as a reasonable machine. Theor. Comput. Sci. 398(1\u20133), 32\u201350 (2008)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"9210_CR11","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1006\/inco.1998.2700","volume":"143","author":"J.-Y. Girard","year":"1998","unstructured":"Girard, J.-Y.: Light linear logic. Inf. Comput. 143(2), 175\u2013204 (1998)","journal-title":"Inf. Comput."},{"key":"9210_CR12","volume-title":"Proof and Types","author":"J.-Y. Girard","year":"1987","unstructured":"Girard, J.-Y., Lafont, Y., Taylor, P.: Proof and Types. Cambridge University Press, Cambridge (1987)"},{"key":"9210_CR13","doi-asserted-by":"crossref","unstructured":"Hofmann, M.: Linear types and non-size-increasing polynomial time computation. In: Proc. of the 14th IEEE Syposium on Logic in Computer Science, pp. 464\u2013473 (1999)","DOI":"10.1109\/LICS.1999.782641"},{"key":"9210_CR14","doi-asserted-by":"crossref","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. Ann. Pure Appl. Logic 104, 113\u2013166 (2000)","journal-title":"Ann. Pure Appl. Logic"},{"issue":"1\u20132","key":"9210_CR15","doi-asserted-by":"crossref","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. Theor. Comput. Sci. 318(1\u20132), 121\u2013137 (2004)","journal-title":"Theor. Comput. Sci."},{"key":"9210_CR16","first-page":"101","volume-title":"Constructivity in Mathematics","author":"G. Kreisel","year":"1959","unstructured":"Kreisel, G.: Interpretation of analysis by means of constructive functions of finite types. In: Heyting,\u00a0A. (ed.) Constructivity in Mathematics, pp. 101\u2013128. North-Holland, Amsterdam (1959)"},{"key":"9210_CR17","doi-asserted-by":"crossref","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. Theor. Comput. Sci. 318, 163\u2013180 (2004)","journal-title":"Theor. Comput. Sci."},{"key":"9210_CR18","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"427","DOI":"10.1007\/3-540-44622-2_29","volume-title":"Proc. of 14th International Workshop on Computer Science Logic","author":"A.S. Murawski","year":"2000","unstructured":"Murawski, A.S., Ong, C.-H.L.: Discreet games, light affine logic and ptime computation. In: Proc. of 14th International Workshop on Computer Science Logic. LNCS, vol. 1862, pp. 427\u2013441. Springer, Berlin (2000)"},{"key":"9210_CR19","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"469","DOI":"10.1007\/3-540-48168-0_33","volume-title":"Proc. of 13th International Workshop on Computer Science Logic","author":"L. Roversi","year":"1999","unstructured":"Roversi, L.: A P-time completeness proof for light logics. In: Proc. of 13th International Workshop on Computer Science Logic. LNCS, vol. 1683, pp. 469\u2013483. Springer, Berlin (1999)"},{"key":"9210_CR20","series-title":"Algorithms and Complexity","first-page":"1","volume-title":"Handbook of Theoretical Computer Science","author":"P. Emde Boas van","year":"1990","unstructured":"van Emde Boas, P.: Machine models and simulation. In: Handbook of Theoretical Computer Science. Algorithms and Complexity, vol.\u00a0A, pp. 1\u201366. MIT Press, Cambridge (1990)"},{"key":"9210_CR21","volume-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"C. Wadsworth","year":"1980","unstructured":"Wadsworth, C.: Some unusual \u03bb-calculus numeral systems. In: Seldin, J.P., Hindley, J.R. (eds.) To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, San Diego (1980)"}],"container-title":["Theory of Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-009-9210-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00224-009-9210-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-009-9210-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,24]],"date-time":"2019-05-24T11:51:38Z","timestamp":1558698698000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00224-009-9210-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,4,7]]},"references-count":21,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2010,5]]}},"alternative-id":["9210"],"URL":"https:\/\/doi.org\/10.1007\/s00224-009-9210-x","relation":{},"ISSN":["1432-4350","1433-0490"],"issn-type":[{"value":"1432-4350","type":"print"},{"value":"1433-0490","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,4,7]]}}}