{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:20:00Z","timestamp":1725484800945},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540430759"},{"type":"electronic","value":"9783540455752"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45575-2_46","type":"book-chapter","created":{"date-parts":[[2007,5,31]],"date-time":"2007-05-31T01:30:22Z","timestamp":1180575022000},"page":"482-493","source":"Crossref","is-referenced-by-count":16,"title":["On Lexicographic Termination Ordering with Space Bound Certifications"],"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","published-online":{"date-parts":[[2001,12,18]]},"reference":[{"key":"46_CR1","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/BF01201998","volume":"2","author":"S. Bellantoni","year":"1992","unstructured":"S. Bellantoni and S. Cook. A new recursion-theoretic characterization of the polytime functions. Computational Complexity, 2:97\u2013110, 1992.","journal-title":"Computational Complexity"},{"key":"46_CR2","unstructured":"R. Benzinger. Automated complexity analysis of NUPRL extracts. PhD thesis, Cornell University, 1999."},{"key":"46_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"372","DOI":"10.1007\/10703163_25","volume-title":"Complexity classes and rewrite systems with polynomial interpretation","author":"G. Bonfante","year":"1999","unstructured":"G. Bonfante, A. Cichon, J-Y Marion, and H. Touzet. Complexity classes and rewrite systems with polynomial interpretation. In Computer Science Logic, 12th International Workshop, CSL\u201998, volume 1584 of Lecture Notes in Computer Science, pages 372\u2013384, 1999."},{"key":"46_CR4","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1145\/322234.322243","volume":"28","author":"A. Chandra","year":"1981","unstructured":"A. Chandra, D. Kozen, and L. Stockmeyer. Alternation. Journal of the ACM, 28:114\u2013133, 1981.","journal-title":"Journal of the ACM"},{"key":"46_CR5","unstructured":"A. Cobham. The intrinsic computational difficulty of functions. In Y. Bar-Hillel, editor, Proceedings of the International Conference on Logic, Methodology, and Philosophy of Science, pages 24\u201330. North-Holland, Amsterdam, 1962."},{"key":"46_CR6","unstructured":"R. Constable and al. Implementing Mathematics with the Nuprl Development System. Prentice-Hall, 1986. http:\/\/www.cs.cornell.edu\/Info\/Projects\/NuPrl\/nuprl.html ."},{"key":"46_CR7","doi-asserted-by":"crossref","unstructured":"K. Crary and S. Weirich. Ressource bound certification. In ACM SIGPLANSIGACT symposium on Principles of programming languages, POPL, pages 184\u2013198, 2000.","DOI":"10.1145\/325694.325716"},{"key":"46_CR8","first-page":"243","volume-title":"Handbook of Theoretical Computer Science","author":"N. Dershowitz","year":"1990","unstructured":"N. Dershowitz and J-P Jouannaud. Handbook of Theoretical Computer Science vol.B, chapter Rewrite systems, pages 243\u2013320. Elsevier Science Publishers B. V. (North-Holland), 1990."},{"issue":"1","key":"46_CR9","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/0304-3975(92)90363-K","volume":"100","author":"A. Goerdt","year":"1992","unstructured":"A. Goerdt. Characterizing complexity classes by higher type primitive recursive definitions. Theoretical Computer Science, 100(1):45\u201366, 1992.","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"46_CR10","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1016\/0304-3975(92)90289-R","volume":"105","author":"D. Hofbauer","year":"1992","unstructured":"D. Hofbauer. Termination proofs with multiset path orderings imply primitive recursive derivation lengths. Theoretical Computer Science, 105(1):129\u2013140, 1992.","journal-title":"Theoretical Computer Science"},{"key":"46_CR11","doi-asserted-by":"crossref","unstructured":"M. Hofmann. Linear types and non-size-increasing polynomial time computation. In Proceedings of the Fourteenth IEEE Symposium on Logic in Computer Science (LICS\u201999), pages 464\u2013473, 1999.","DOI":"10.1109\/LICS.1999.782641"},{"key":"46_CR12","doi-asserted-by":"crossref","unstructured":"M. Hofmann. A type system for bounded space and functional in-place update. In European Symposium on Programming, ESOP\u201900, volume 1782 of Lecture Notes in Computer Science, pages 165\u2013179, 2000.","DOI":"10.1007\/3-540-46425-5_11"},{"key":"46_CR13","doi-asserted-by":"crossref","unstructured":"N. Immerman. Descriptive Complexity. Springer, 1999.","DOI":"10.1007\/978-1-4612-0539-5"},{"key":"46_CR14","doi-asserted-by":"crossref","unstructured":"N. Jones. The Expressive Power of Higher order Types or, Life without CONS. to appear, 2000.","DOI":"10.1017\/S0956796800003889"},{"key":"46_CR15","unstructured":"S. Kamin and J-J L\u00e9vy. Attempts for generalising the recursive path orderings. Technical report, Univerity of Illinois, Urbana, 1980. Unpublished note."},{"issue":"2\u20133","key":"46_CR16","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/0304-3975(85)90175-6","volume":"40","author":"M. S. Krishnamoorthy","year":"1985","unstructured":"M. S. Krishnamoorthy and P. Narendran. On recursive path ordering. Theoretical Computer Science, 40(2\u20133):323\u2013328, October 1985.","journal-title":"Theoretical Computer Science"},{"key":"46_CR17","unstructured":"D.S. Lankford. On proving term rewriting systems are noetherien. Technical Report MTP-3, Louisiana Technical University, 1979."},{"key":"46_CR18","doi-asserted-by":"crossref","unstructured":"D. Leivant. Predicative recurrence and computational complexity I: Word recurrence and poly-time. In Peter Clote and Jeffery Remmel, editors, Feasible Mathematics II, pages 320\u2013343. Birkh\u00e4user, 1994.","DOI":"10.1007\/978-1-4612-2566-9_11"},{"key":"46_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"486","DOI":"10.1007\/BFb0022277","volume-title":"Ramified recurrence and computational complexityII: substitution and poly-space","author":"D. Leivant","year":"1995","unstructured":"D. Leivant and J-Y Marion. Ramified recurrence and computational complexityII: substitution and poly-space. In L. Pacholski and J. Tiuryn, editors, Computer Science Logic, 8th Workshop, CSL\u201994, volume 933 of Lecture Notes in Computer Science, pages 486\u2013500, Kazimierz,Poland, 1995. Springer."},{"key":"46_CR20","unstructured":"J-Y Marion. Complexit\u00e9 implicite des calculs, de la th\u00e9orie \u00e0 la pratique, 2000. Habilitation."},{"key":"46_CR21","series-title":"Lect Notes Comput Sci","first-page":"25","volume-title":"LPAR","author":"J.-Y. Marion","year":"2000","unstructured":"J-Y Marion and J-Y Moyen. Efficient first order functional program interpreter with time bound certifications. In LPAR, volume 1955 of Lecture Notes in Computer Science, pages 25\u201342. Springer, Nov 2000."},{"key":"46_CR22","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/BF01706069","volume":"6","author":"D.B. Thompson","year":"1972","unstructured":"D.B. Thompson. Subrecursiveness: machine independent notions of computability in restricted time and storage. Math. System Theory, 6:3\u201315, 1972.","journal-title":"Math. System Theory"},{"key":"46_CR23","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1016\/0304-3975(94)00135-6","volume":"139","author":"A. Weiermann","year":"1995","unstructured":"A. Weiermann. Termination proofs by lexicographic path orderings yield multiply recursive derivation lengths. Theoretical Computer Science, 139:335\u2013362, 1995.","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Perspectives of System Informatics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45575-2_46","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,12]],"date-time":"2023-05-12T02:46:05Z","timestamp":1683859565000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45575-2_46"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540430759","9783540455752"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-45575-2_46","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}