{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:34Z","timestamp":1761611194188},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665403"},{"type":"electronic","value":"9783540481645"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/10704567_2","type":"book-chapter","created":{"date-parts":[[2006,12,28]],"date-time":"2006-12-28T23:27:08Z","timestamp":1167348428000},"page":"29-46","source":"Crossref","is-referenced-by-count":2,"title":["On Formalised Proofs of Termination of Recursive Functions"],"prefix":"10.1007","author":[{"given":"Fairouz","family":"Kamareddine","sequence":"first","affiliation":[]},{"given":"Fran\u00e7ois","family":"Monin","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"2_CR1","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1016\/0167-6423(87)90030-X","volume":"9","author":"A. Ben Cherifa","year":"1987","unstructured":"Ben Cherifa, A., Lescanne, P.: Termination of rewriting systems by polynomial interpretations and its implementation. Science of Computer Programming\u00a09(2), 137\u2013159 (1987)","journal-title":"Science of Computer Programming"},{"key":"2_CR2","volume-title":"A computational logic","author":"R.S. Boyer","year":"1979","unstructured":"Boyer, R.S., Moore, J.S.: A computational logic. Academic Press, New York (1979)"},{"key":"2_CR3","volume-title":"A computational logic handbook","author":"R.S. Boyer","year":"1988","unstructured":"Boyer, R.S., Moore, J.S.: A computational logic handbook. Academic Press, London (1988)"},{"key":"2_CR4","unstructured":"Cornes, C., et al.: The Coq proof assistant reference manual version 5.10. Technical Report 077, INRIA (1995)"},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"Rewriting Techniques and Applications","author":"J. Giesl","year":"1995","unstructured":"Giesl, J.: Generating polynomial orderings for termination proofs. In: Hsiang, J. (ed.) RTA 1995. LNCS, vol.\u00a0914. Springer, Heidelberg (1995)"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","volume-title":"KI-95: Advances in Artificial Intelligence","author":"J. Giesl","year":"1995","unstructured":"Giesl, J.: Automated termination proofs with measure functions. In: Wachsmuth, I., Brauer, W., Rollinger, C.-R. (eds.) KI 1995. LNCS, vol.\u00a0981. Springer, Heidelberg (1995)"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"Static Analysis","author":"J. Giesl","year":"1995","unstructured":"Giesl, J.: Termination analysis for functional programs using term orderings. In: Mycroft, A. (ed.) SAS 1995. LNCS, vol.\u00a0983. Springer, Heidelberg (1995)"},{"key":"2_CR8","unstructured":"Kamareddine, F.D., Monin, F.: On Formalised Proofs of Termination of Recursive Function. \n                  \n                    http:\/\/www.cee.hw.ac.uk\/fairouz\/papers\/research-reports\/ppdp99full.ps"},{"issue":"3","key":"2_CR9","first-page":"149","volume":"26","author":"J.L. Krivine","year":"1990","unstructured":"Krivine, J.L., Parigot, M.: Programming with proofs. J. Inf. Process Cybern.\u00a0EIK 26(3), 149\u2013167 (1990)","journal-title":"J. Inf. Process Cybern. EIK"},{"key":"2_CR10","unstructured":"Lankford, D.S.: On proving term rewriting systems are Noetherian. Techinical report Memo MTP-3, Louisiana Technology University (1979)"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"Types for Proofs and Programs","author":"P. Manoury","year":"1995","unstructured":"Manoury, P.: A User\u2019s friendly syntax to define recursive functions as typed lambdaterms. In: Smith, J., Dybjer, P., Nordstr\u00f6m, B. (eds.) TYPES 1994. LNCS, vol.\u00a0996. Springer, Heidelberg (1995)"},{"key":"2_CR12","unstructured":"Manoury, P., Simonot, M.: Des preuves de totalit\u00e9 de fonctions comme synth\u00e8se de programmes. PhD thesis, University Paris 7 (1992)"},{"issue":"2","key":"2_CR13","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1016\/0304-3975(94)00021-2","volume":"135","author":"P. Manoury","year":"1994","unstructured":"Manoury, P., Simonot, M.: Automatizing termination proofs of recursively defined functions. Theoretical Computer Science\u00a0135(2), 319\u2013343 (1994)","journal-title":"Theoretical Computer Science"},{"key":"2_CR14","unstructured":"Monin, F., Simonot, M.: An ordinal measure based procedure for termination of functions. To appear in Theoretical Computer Science"},{"issue":"2","key":"2_CR15","first-page":"144","volume":"3","author":"F. Nielson","year":"1996","unstructured":"Nielson, F., Nielson, H.R.: Operational semantics of termination types. Nordic Journal of Computing\u00a03(2), 144\u2013187 (1996)","journal-title":"Nordic Journal of Computing"},{"issue":"2","key":"2_CR16","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1016\/0304-3975(92)90042-E","volume":"94","author":"M. Parigot","year":"1992","unstructured":"Parigot, M.: Recursive programming with proofs. Theoretical Computer Science\u00a094(2), 335\u2013356 (1992)","journal-title":"Theoretical Computer Science"},{"key":"2_CR17","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/0020-0190(94)90032-9","volume":"49","author":"J. Steinbach","year":"1994","unstructured":"Steinbach, J.: Generating polynomial orderings. Information Processing Letters\u00a049, 85\u201393 (1994)","journal-title":"Information Processing Letters"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0012861","volume-title":"9th International Conference on Automated Deduction","author":"C. Walther","year":"1988","unstructured":"Walther, C.: Argument-bounded algorithms as a basis for automated termination proofs. In: Lusk, E.\u2018., Overbeek, R. (eds.) CADE 1988. LNCS, vol.\u00a0310. Springer, Heidelberg (1988)"},{"issue":"1","key":"2_CR19","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/0004-3702(94)90063-9","volume":"71","author":"C. Walther","year":"1994","unstructured":"Walther, C.: On proving the termination of algorithms by machine. Artificial intelligence\u00a071(1), 101\u2013157 (1994)","journal-title":"Artificial intelligence"}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10704567_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,18]],"date-time":"2019-03-18T03:24:42Z","timestamp":1552879482000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10704567_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665403","9783540481645"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/10704567_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]}}}