{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:04:14Z","timestamp":1725566654696},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540255963"},{"type":"electronic","value":"9783540320333"}],"license":[{"start":{"date-parts":[[2005,1,1]],"date-time":"2005-01-01T00:00:00Z","timestamp":1104537600000},"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":[[2005]]},"DOI":"10.1007\/978-3-540-32033-3_12","type":"book-chapter","created":{"date-parts":[[2010,9,28]],"date-time":"2010-09-28T00:20:02Z","timestamp":1285633202000},"page":"150-164","source":"Crossref","is-referenced-by-count":10,"title":["Quasi-interpretations and Small Space Bounds"],"prefix":"10.1007","author":[{"given":"Guillaume","family":"Bonfante","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Yves","family":"Marion","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Yves","family":"Moyen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","unstructured":"Benzinger, R.: Automated complexity analysis of NUPRL extracts. PhD thesis, Cornell University (1999)"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","volume-title":"Rewriting Techniques and Applications","author":"D. Hofbauer","year":"1989","unstructured":"Hofbauer, D., Lautemann, C.: Termination proofs and the length of derivations. In: Dershowitz, N. (ed.) RTA 1989. LNCS, vol.\u00a0355, Springer, Heidelberg (1989)"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1007\/3-540-55602-8_161","volume-title":"Automated Deduction - CADE-11","author":"E. Cichon","year":"1992","unstructured":"Cichon, E., Lescanne, P.: Polynomial interpretations and the complexity of algorithms. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 139\u2013147. Springer, Heidelberg (1992)"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Bonfante, G., Cichon, A., Marion, J.Y., Touzet, H.: Algorithms with polynomial interpretation termination proof. Journal of Functional Programming\u00a011 (2000)","DOI":"10.1017\/S0956796800003877"},{"key":"12_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/3-540-44404-1_3","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":"12_CR6","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, p. 482. Springer, Heidelberg (2001)"},{"key":"12_CR7","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1016\/0304-3975(92)90289-R","volume":"105","author":"D. Hofbauer","year":"1992","unstructured":"Hofbauer, D.: Termination proofs with multiset path orderings imply primitive recursive derivation lengths. Theoretical Computer Science\u00a0105, 129\u2013140 (1992)","journal-title":"Theoretical Computer Science"},{"key":"12_CR8","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1016\/0304-3975(94)00135-6","volume":"139","author":"A. Weiermann","year":"1995","unstructured":"Weiermann, A.: Termination proofs by lexicographic path orderings yield multiply recursive derivation lengths. Theoretical Computer Science\u00a0139, 335\u2013362 (1995)","journal-title":"Theoretical Computer Science"},{"key":"12_CR9","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1090\/S0002-9947-1963-0158822-2","volume":"106","author":"R. Ritchie","year":"1963","unstructured":"Ritchie, R.: Classes of predictably computable functions. Transaction of the American Mathematical Society\u00a0106, 139\u2013173 (1963)","journal-title":"Transaction of the American Mathematical Society"},{"key":"12_CR10","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/s001530050054","volume":"36","author":"A. Beckmann","year":"1996","unstructured":"Beckmann, A., Weiermann, A.: A term rewriting characterization of the polytime functions and related complexity classes. Archive for Mathematical Logic\u00a036, 11\u201330 (1996)","journal-title":"Archive for Mathematical Logic"},{"key":"12_CR11","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, 2\u201318 (2003)","journal-title":"Information and Computation"},{"key":"12_CR12","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, 97\u2013110 (1992)","journal-title":"Computational Complexity"},{"key":"12_CR13","first-page":"320","volume-title":"Feasible Mathematics II","author":"D. Leivant","year":"1994","unstructured":"Leivant, D.: Predicative recurrence and computational complexity I: Word recurrence and poly-time. In: Clote, P., Remmel, J. (eds.) Feasible Mathematics II, pp. 320\u2013343. Birkh\u00e4user, Basel (1994)"},{"key":"12_CR14","doi-asserted-by":"crossref","first-page":"167","DOI":"10.3233\/FI-1993-191-207","volume":"19","author":"D. Leivant","year":"1993","unstructured":"Leivant, D., Marion, J.Y.: Lambda calculus characterizations of poly-time. Fundamenta Informaticae\u00a019, 167 (1993)","journal-title":"Fundamenta Informaticae"},{"key":"12_CR15","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1016\/S0304-3975(98)00357-0","volume":"228","author":"N.D. Jones","year":"1999","unstructured":"Jones, N.D.: LOGSPACE and PTIME characterized by programming languages. Theoretical Computer Science\u00a0228, 151\u2013174 (1999)","journal-title":"Theoretical Computer Science"},{"key":"12_CR16","first-page":"210","volume-title":"Twenty Fourth Symposium on Foundations of Computer Science","author":"Y. Gurevich","year":"1983","unstructured":"Gurevich, Y.: Algebras of feasible functions. In: Twenty Fourth Symposium on Foundations of Computer Science, pp. 210\u2013214. IEEE Computer Society Press, Los Alamitos (1983)"},{"key":"12_CR17","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/s001530200002","volume":"41","author":"I. Oitavem","year":"2002","unstructured":"Oitavem, I.: A term rewriting characterization of the functions computable in polynomial space. Archive for Mathematical Logic\u00a041, 35\u201347 (2002)","journal-title":"Archive for Mathematical Logic"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"Amadio, R., Coupet-Grimal, S., Zilio, S.D., Jakubiec, L.: A functional scenario for bytecode verification of resource bounds. In: CSL. (2004) (to appear)","DOI":"10.1007\/978-3-540-30124-0_22"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Amadio, R.M., Dal-Zilio, S.: Resource control for synchronous cooperative threads. In: CONCUR, pp. 68\u201382 (2004)","DOI":"10.1007\/978-3-540-28644-8_5"},{"key":"12_CR20","unstructured":"Bonfante, G., Marion, J.Y., Moyen, J.Y., P\u00e9choux, R.: Synthesis of quasiinterpretations. Technical report, Loria (2005) Submited to RULE 2005, Available at http:\/\/www.loria.fr\/~bonfante\/publis\/RULE05.pdf"},{"key":"12_CR21","unstructured":"Bonfante, G., Marion, J.Y., Moyen, J.Y.: Quasi-interpretations. Technical report, Loria (2004) Submited to Theoretical Computer Science, accessible: http:\/\/www.loria.fr\/~moyen\/"},{"key":"12_CR22","doi-asserted-by":"publisher","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"G. Huet","year":"1980","unstructured":"Huet, G.: Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the ACM\u00a027, 797\u2013821 (1980)","journal-title":"Journal of the ACM"},{"key":"12_CR23","doi-asserted-by":"publisher","first-page":"952","DOI":"10.2307\/2275767","volume":"60","author":"E. Gr\u00e4del","year":"1995","unstructured":"Gr\u00e4del, E., Gurevich, Y.: Tailoring recursion for complexity. Journal of Symbolic Logic\u00a060, 952\u2013969 (1995)","journal-title":"Journal of Symbolic Logic"},{"key":"12_CR24","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"Dershowitz, N.: Orderings for term-rewriting systems. Theoretical Computer Science\u00a017, 279\u2013301 (1982)","journal-title":"Theoretical Computer Science"},{"key":"12_CR25","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/0304-3975(85)90175-6","volume":"40","author":"M.S. Krishnamoorthy","year":"1985","unstructured":"Krishnamoorthy, M.S., Narendran, P.: On recursive path ordering. Theoretical Computer Science\u00a040, 323\u2013328 (1985)","journal-title":"Theoretical Computer Science"},{"key":"12_CR26","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/S0304-3975(99)00207-8","volume":"236","author":"T. Arts","year":"2000","unstructured":"Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science\u00a0236, 133\u2013178 (2000)","journal-title":"Theoretical Computer Science"},{"key":"12_CR27","doi-asserted-by":"crossref","unstructured":"Bonfante, G., Marion, J.Y., Moyen, J.Y.: Quasi-interpretations and small space bounds. Technical report, Loria (2005), http:\/\/www.loria.fr\/~bonfante\/publis\/RTA05f.pdf","DOI":"10.1007\/978-3-540-32033-3_12"},{"key":"12_CR28","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1016\/0020-0190(79)90071-1","volume":"9","author":"N. Dershowitz","year":"1979","unstructured":"Dershowitz, N.: A note on simplification ordering. Information Processing Letters\u00a09, 212\u2013215 (1979)","journal-title":"Information Processing Letters"},{"key":"12_CR29","unstructured":"Bonfante, G.: Constructions d\u2019ordres, analyse de la complexit\u00e9. Th\u00e8se, Institut National Polytechnique de Lorraine (2000)"}],"container-title":["Lecture Notes in Computer Science","Term Rewriting and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-32033-3_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,10]],"date-time":"2021-11-10T19:02:58Z","timestamp":1636570978000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-32033-3_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540255963","9783540320333"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-32033-3_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}