{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:13:33Z","timestamp":1725491613372},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540752905"},{"type":"electronic","value":"9783540752929"}],"license":[{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"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":[[2007]]},"DOI":"10.1007\/978-3-540-75292-9_28","type":"book-chapter","created":{"date-parts":[[2007,9,11]],"date-time":"2007-09-11T10:43:07Z","timestamp":1189507387000},"page":"410-424","source":"Crossref","is-referenced-by-count":4,"title":["Quasi-interpretation Synthesis by Decomposition"],"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":"Romain","family":"P\u00e9choux","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"28_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/3-540-44904-3_3","volume-title":"Typed Lambda Calculi and Applications","author":"R. Amadio","year":"2003","unstructured":"Amadio, R.: Max-plus quasi-interpretations. In: Hofmann, M.O. (ed.) TLCA 2003. LNCS, vol.\u00a02701, pp. 31\u201345. Springer, Heidelberg (2003)"},{"key":"28_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/978-3-540-30124-0_22","volume-title":"Computer Science Logic","author":"R. Amadio","year":"2004","unstructured":"Amadio, R., Coupet-Grimal, S., Dal-Zilio, S., Jakubiec, L.: A functional scenario for bytecode verification of resource bounds. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol.\u00a03210, pp. 265\u2013279. Springer, Heidelberg (2004)"},{"key":"28_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/978-3-540-28644-8_5","volume-title":"CONCUR 2004 - Concurrency Theory","author":"R. Amadio","year":"2004","unstructured":"Amadio, R., Dal-Zilio, S.: Resource control for synchronous cooperative threads. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, pp. 68\u201382. Springer, Heidelberg (2004)"},{"key":"28_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1007\/11417170_6","volume-title":"Typed Lambda Calculi and Applications","author":"P. Baillot","year":"2005","unstructured":"Baillot, P., Terui, K.: A feasible algorithm for typing in elementary affine logic. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol.\u00a03461, pp. 55\u201370. Springer, Heidelberg (2005)"},{"key":"28_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Springer, Heidelberg (2001)"},{"key":"28_CR6","unstructured":"Bonfante, G., Marion, J.-Y., Moyen, J.-Y.: Quasi-interpretation a way to control resources. Theoretical Computer Science (2005) (submitted), \n                  \n                    http:\/\/www.loria.fr\/~marionjy"},{"key":"28_CR7","unstructured":"Bonfante, G., Marion, J.-Y., Moyen, J.-Y., P\u00e9choux, R.: Synthesis of quasi-interpretations. In: LCC2005, LICS affiliated Workshop (2005), \n                  \n                    http:\/\/hal.inria.fr\/"},{"issue":"1-2","key":"28_CR8","first-page":"87","volume":"65","author":"P. Coppola","year":"2005","unstructured":"Coppola, P., Rocca, S.R.D.: Principal typing for lambda calculus in elementary affine logic. Fundamenta Informaticae\u00a065(1-2), 87\u2013112 (2005)","journal-title":"Fundamenta Informaticae"},{"key":"28_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/11575467_17","volume-title":"Programming Languages and Systems","author":"S. Dal-Zilio","year":"2005","unstructured":"Dal-Zilio, S., Gascon, R.: Resource bound certification for a tail-recursive virtual machine. In: Yi, K. (ed.) APLAS 2005. LNCS, vol.\u00a03780, pp. 247\u2013263. Springer, Heidelberg (2005)"},{"key":"28_CR10","unstructured":"Danvy, O.: An analytical approach to programs as data objects, Doctor Scientarum degree in Computer Science. BRICS. Departement of Computer Science. University of Aarhus (2006)"},{"issue":"3","key":"28_CR11","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(3), 279\u2013301 (1982)","journal-title":"Theoretical Computer Science"},{"key":"28_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-60381-6","volume-title":"CTRS 1994","author":"N. Dershowitz","year":"1995","unstructured":"Dershowitz, N.: Hierachical termination. In: Lindenstrauss, N., Dershowitz, N. (eds.) CTRS 1994. LNCS, vol.\u00a0968, Springer, Heidelberg (1995)"},{"issue":"2","key":"28_CR13","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":"28_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/BFb0013819","volume-title":"ALP 1992","author":"B. Gramlich","year":"1992","unstructured":"Gramlich, B.: Generalized sufficient conditions for modular termination of rewriting. In: Kirchner, H., Levi, G. (eds.) ALP 1992. LNCS, vol.\u00a0632, pp. 53\u201368. Springer, Heidelberg (1992)"},{"issue":"4","key":"28_CR15","first-page":"258","volume":"7","author":"M. Hofmann","year":"2000","unstructured":"Hofmann, M.: A type system for bounded space and functional in-place update. Nordic Journal of Computing\u00a07(4), 258\u2013289 (2000)","journal-title":"Nordic Journal of Computing"},{"key":"28_CR16","doi-asserted-by":"crossref","unstructured":"Hofmann, M.: The strength of Non-Size Increasing computation. In: POPL, pp. 260\u2013269 (2002)","DOI":"10.1145\/565816.503297"},{"issue":"4","key":"28_CR17","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(4), 797\u2013821 (1980)","journal-title":"Journal of the ACM"},{"key":"28_CR18","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2003.001.0001","volume-title":"Computability and complexity, from a programming perspective","author":"N.D. Jones","year":"1997","unstructured":"Jones, N.D.: Computability and complexity, from a programming perspective. MIT Press, Cambridge (1997)"},{"key":"28_CR19","first-page":"1","volume-title":"Handbook of logic in Computer Science","author":"J.W. Klop","year":"1992","unstructured":"Klop, J.W.: Term rewriting systems. In: Handbook of logic in Computer Science, vol.\u00a02, pp. 1\u2013116. Oxford University Press, Oxford (1992)"},{"key":"28_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/11494645_33","volume-title":"New Computational Paradigms","author":"L. Kristiansen","year":"2005","unstructured":"Kristiansen, L., Jones, N.D.: The flow of data and the complexity of algorithms. In: Cooper, S.B., L\u00f6we, B., Torenvliet, L. (eds.) CiE 2005. LNCS, vol.\u00a03526, pp. 263\u2013274. Springer, Heidelberg (2005)"},{"key":"28_CR21","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/0304-3975(92)90015-8","volume":"103","author":"M. Kurihara","year":"1992","unstructured":"Kurihara, M., Ohuchi, A.: Modularity of simple termination of term rewriting systems with shared constructors. Theoretical Computer Science\u00a0103, 273\u2013282 (1992)","journal-title":"Theoretical Computer Science"},{"key":"28_CR22","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"},{"key":"28_CR23","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":"28_CR24","unstructured":"Marion, J.-Y., Moyen, J.-Y.: Heap analysis for assembly programs. Technical report, Loria (2006)"},{"key":"28_CR25","unstructured":"Middeldorp, A.: Modular properties of term rewriting Systems. PhD thesis, Vrije Universiteit te Amsterdam (1990)"},{"issue":"5","key":"28_CR26","doi-asserted-by":"publisher","first-page":"1122","DOI":"10.1137\/S0097539704445597","volume":"35","author":"K.-H. Niggl","year":"2006","unstructured":"Niggl, K.-H., Wunderlich, H.: Certifying polynomial time and linear\/polynomial space for imperative programs. SIAM Journal on Computing\u00a035(5), 1122\u20131147 (2006)","journal-title":"SIAM Journal on Computing"},{"key":"28_CR27","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3661-8","volume-title":"Advanced Topics in Term Rewriting","author":"E. Ohlebusch","year":"2002","unstructured":"Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer, Heidelberg (2002)"},{"key":"28_CR28","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1016\/0304-3975(95)00075-8","volume":"151","author":"M.R.K. Krishna Rao","year":"1995","unstructured":"Krishna Rao, M.R.K.: Modular proofs of completeness of hierarchical term rewriting systems. Theoretical Computer Science\u00a0151, 487\u2013512 (1995)","journal-title":"Theoretical Computer Science"},{"key":"28_CR29","first-page":"717","volume-title":"ACM","author":"J.C. Reynolds","year":"1972","unstructured":"Reynolds, J.C.: Definitional interpreters for higher-order programming languages. In: ACM, pp. 717\u2013740. ACM Press, New York (1972)"},{"key":"28_CR30","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1016\/0020-0190(87)90122-0","volume":"25","author":"Y. Toyama","year":"1987","unstructured":"Toyama, Y.: Counterexamples for the direct sum of term rewriting systems. Information Processing Letters\u00a025, 141\u2013143 (1987)","journal-title":"Information Processing Letters"},{"issue":"1","key":"28_CR31","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1145\/7531.7534","volume":"34","author":"Y. Toyama","year":"1987","unstructured":"Toyama, Y.: On the church-rosser property for the direct sum of term rewriting systems. Journal of the ACM\u00a034(1), 128\u2013143 (1987)","journal-title":"Journal of the ACM"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2007"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-75292-9_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,8]],"date-time":"2020-01-08T18:08:16Z","timestamp":1578506896000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-75292-9_28"}},"subtitle":["An Application to Higher-Order Programs"],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540752905","9783540752929"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-75292-9_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}