{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:21:42Z","timestamp":1751660502764,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642119569"},{"type":"electronic","value":"9783642119576"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-11957-6_7","type":"book-chapter","created":{"date-parts":[[2010,3,8]],"date-time":"2010-03-08T00:55:38Z","timestamp":1268009738000},"page":"104-124","source":"Crossref","is-referenced-by-count":12,"title":["A PolyTime Functional Language from Light Linear Logic"],"prefix":"10.1007","author":[{"given":"Patrick","family":"Baillot","sequence":"first","affiliation":[]},{"given":"Marco","family":"Gaboardi","sequence":"additional","affiliation":[]},{"given":"Virgile","family":"Mogbil","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"7_CR1","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/BF01201998","volume":"2","author":"S. Bellantoni","year":"1992","unstructured":"Bellantoni, S., Cook, S.: A new recursion-theoretic characterization of the polytime functions. Computational Complexity\u00a02(2), 97\u2013110 (1992)","journal-title":"Computational Complexity"},{"key":"7_CR2","first-page":"2","volume-title":"LICS 1991","author":"D. Leivant","year":"1991","unstructured":"Leivant, D.: A foundational delineation of computational feasibility. In: Meyer, A.R. (ed.) LICS 1991, pp. 2\u201311. IEEE Computer Society, Los Alamitos (1991)"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/BFb0037112","volume-title":"Typed Lambda Calculi and Applications","author":"D. Leivant","year":"1993","unstructured":"Leivant, D., Marion, J.Y.: Lambda calculus characterizations of poly-time. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664, pp. 274\u2013288. Springer, Heidelberg (1993)"},{"issue":"2","key":"7_CR4","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"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Hofmann, M.: Linear types and non-size-increasing polynomial time computation. In: LICS 1999, pp. 464\u2013473 (1999)","DOI":"10.1109\/LICS.1999.782641"},{"key":"7_CR6","series-title":"Lecture Notes in Artificial Intelligence","first-page":"25","volume-title":"Logic for Programming and Automated Reasoning","author":"J.Y. Marion","year":"2000","unstructured":"Marion, J.Y., Moyen, J.Y.: Efficient first order functional program interpreter with time bound certifications. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS (LNAI), vol.\u00a01955, pp. 25\u201342. Springer, Heidelberg (2000)"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Hughes, J., Pareto, L.: Recursion and dynamic data-structures in bounded space: Towards embedded ML programming. In: ACM ICFP 1999, pp. 70\u201381 (1999)","DOI":"10.1145\/317765.317785"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Hofmann, M., Jost, S.: Static prediction of heap usage for first-order functional programs. In: ACM POPL 2003, New Orleans, LA, USA (2003)","DOI":"10.1145\/604131.604148"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Crary, K., Weirich, S.: Resource bound certification. In: ACM POPL 2000, pp. 184\u2013198 (2000)","DOI":"10.1145\/325694.325716"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/11874683_10","volume-title":"Computer Science Logic","author":"V. Atassi","year":"2006","unstructured":"Atassi, V., Baillot, P., Terui, K.: Verification of ptime reducibility for system F terms via dual light affine logic. In: \u00c9sik, Z. (ed.) CSL 2006. LNCS, vol.\u00a04207, pp. 150\u2013166. Springer, Heidelberg (2006)"},{"key":"7_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.Y. Girard","year":"1987","unstructured":"Girard, J.Y.: Linear logic. TCS\u00a050, 1\u2013102 (1987)","journal-title":"TCS"},{"issue":"1","key":"7_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(92)90386-T","volume":"97","author":"J.Y. Girard","year":"1992","unstructured":"Girard, J.Y., Scedrov, A., Scott, P.J.: Bounded linear logic: a modular approach to polynomial-time computability. TCS\u00a097(1), 1\u201366 (1992)","journal-title":"TCS"},{"issue":"1-2","key":"7_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. TCS\u00a0318(1-2), 163\u2013180 (2004)","journal-title":"TCS"},{"key":"7_CR14","first-page":"209","volume-title":"LICS 2001","author":"K. Terui","year":"2001","unstructured":"Terui, K.: Light affine lambda calculus and polytime strong normalization. In: LICS 2001, pp. 209\u2013220. IEEE Computer Society, Los Alamitos (2001)"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1007\/978-3-540-24727-2_4","volume-title":"Foundations of Software Science and Computation Structures","author":"P. Baillot","year":"2004","unstructured":"Baillot, P., Mogbil, V.: Soft lambda-calculus: a language for polynomial time computation. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol.\u00a02987, pp. 27\u201341. Springer, Heidelberg (2004)"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"Baillot, P.: Checking polynomial time complexity with types. In: Proceedings of the 2nd IFIP International Conference on TCS, pp. 370\u2013382 (2002)","DOI":"10.1007\/978-0-387-35608-2_31"},{"issue":"1","key":"7_CR17","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.ic.2008.08.005","volume":"207","author":"P. Baillot","year":"2009","unstructured":"Baillot, P., Terui, K.: Light types for polynomial time computation in lambda calculus. Information and Computation\u00a0207(1), 41\u201362 (2009)","journal-title":"Information and Computation"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-540-74915-8_21","volume-title":"Computer Science Logic","author":"M. Gaboardi","year":"2007","unstructured":"Gaboardi, M., Ronchi Della Rocca, S.: A soft type assignment system for \u03bb-calculus. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol.\u00a04646, pp. 253\u2013267. Springer, Heidelberg (2007)"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-642-02444-3_9","volume-title":"Types for Proofs and Programs","author":"M. Gaboardi","year":"2009","unstructured":"Gaboardi, M., Ronchi Della Rocca, S.: Type inference for a polynomial lambda calculus. In: Berardi, S., Damiani, F., de\u2019Liguoro, U. (eds.) TYPES 2008. LNCS, vol.\u00a05497, pp. 136\u2013152. Springer, Heidelberg (2009)"},{"key":"7_CR20","first-page":"17","volume":"104","author":"S. Bellantoni","year":"2000","unstructured":"Bellantoni, S., Niggl, K.H., Schwichtenberg, H.: Higher type recursion, ramification and polynomial time. APAL\u00a0104, 17\u201330 (2000)","journal-title":"APAL"},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"178","DOI":"10.1007\/978-3-540-24849-1_12","volume-title":"Types for Proofs and Programs","author":"U. Lago Dal","year":"2004","unstructured":"Dal Lago, U., Martini, S., Roversi, L.: Higher order linear ramified recurrence. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol.\u00a03085, pp. 178\u2013193. Springer, Heidelberg (2004)"},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"Dal Lago, U.: The geometry of linear higher-order recursion. ACM TOCL\u00a010(2) (2009)","DOI":"10.1145\/1462179.1462180"},{"issue":"1","key":"7_CR23","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/S0890-5401(03)00011-7","volume":"183","author":"J.Y. Marion","year":"2003","unstructured":"Marion, J.Y.: Analysing the implicit complexity of programs. Information and Computation\u00a0183(1), 2\u201318 (2003)","journal-title":"Information and Computation"},{"key":"7_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"482","DOI":"10.1007\/3-540-45575-2_46","volume-title":"Perspectives of System Informatics","author":"G. Bonfante","year":"2001","unstructured":"Bonfante, G., Marion, J.Y., Moyen, J.Y.: On lexicographic termination ordering with space bound certifications. In: Bj\u00f8rner, D., Broy, M., Zamulin, A.V. (eds.) PSI 2001. LNCS, vol.\u00a02244, pp. 482\u2013493. Springer, Heidelberg (2001)"},{"issue":"1-2","key":"7_CR25","first-page":"29","volume":"65","author":"R.M. Amadio","year":"2005","unstructured":"Amadio, R.M.: Synthesis of max-plus quasi-interpretations. Fundamenta Informaticae\u00a065(1-2), 29\u201360 (2005)","journal-title":"Fundamenta Informaticae"},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"Marion, J.Y., P\u00e9choux, R.: Characterizations of polynomial complexity classes with a better intensionality. In: ACM-PPDP 2008, pp. 79\u201388 (2008)","DOI":"10.1145\/1389449.1389460"},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"Marion, J.Y., P\u00e9choux, R.: Sup-interpretations, a semantic method for static analysis of program resources. ACM TOCL\u00a010(4) (2009)","DOI":"10.1145\/1555746.1555751"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-11957-6_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T01:37:58Z","timestamp":1739929078000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11957-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642119569","9783642119576"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11957-6_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}