{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:24:26Z","timestamp":1761611066882},"reference-count":18,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[2001,3,1]],"date-time":"2001-03-01T00:00:00Z","timestamp":983404800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":4521,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2001,3]]},"DOI":"10.1016\/s0304-3975(99)00118-8","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T16:01:16Z","timestamp":1027612876000},"page":"63-94","source":"Crossref","is-referenced-by-count":4,"title":["An ordinal measure based procedure for termination of functions"],"prefix":"10.1016","volume":"254","author":[{"given":"Fran\u00e7ois","family":"Monin","sequence":"first","affiliation":[]},{"given":"Marianne","family":"Simonot","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(99)00118-8_BIB1","series-title":"A Computational Logic","author":"Boyer","year":"1979"},{"key":"10.1016\/S0304-3975(99)00118-8_BIB2","unstructured":"R.S. Boyer, J S. Moore, A Computational Logic Handbook, Academic Press, 1988."},{"key":"10.1016\/S0304-3975(99)00118-8_BIB3","series-title":"Integrating decision procedures into heuristic theorem provers","author":"Boyer","year":"1988"},{"key":"10.1016\/S0304-3975(99)00118-8_BIB4","doi-asserted-by":"crossref","unstructured":"E.A. Cichon, H. Touzet, An ordinal calculus for proving termination in term rewriting, in: H. Kirchner (Ed.), Proc. 21st Internat. Colloquium on Trees in Algebra and Programming, CAAP\u201996, Lecture Notes in Computer Science, vol. 1059, 1996, pp. 226\u2013240.","DOI":"10.1007\/3-540-61064-2_40"},{"key":"10.1016\/S0304-3975(99)00118-8_BIB5","unstructured":"C. Cornes et al., The Coq proof assistant reference manual version 5.10, Technical Report 077, INRIA, 1995."},{"key":"10.1016\/S0304-3975(99)00118-8_BIB6","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1023\/A:1005797629953","article-title":"Termination of nested and mutually recursive algorithms","volume":"19","author":"Giesl","year":"1997","journal-title":"J. Automat. Reason."},{"key":"10.1016\/S0304-3975(99)00118-8_BIB7","series-title":"Lambda-Calculus, Types and Models, Computers and their Applications","author":"Krivine","year":"1993"},{"key":"10.1016\/S0304-3975(99)00118-8_BIB8","first-page":"149","article-title":"Programming with proofs","volume":"26(3)","author":"Krivine","year":"1990","journal-title":"J. Inform. Process. Cybernet. EIK"},{"key":"10.1016\/S0304-3975(99)00118-8_BIB9","unstructured":"P. Manoury, M. Simonot, Des preuves de totalit\u00e9 de fonctions comme synth\u00e8se de programmes, Ph.D. Thesis, University Paris 7, 1992."},{"key":"10.1016\/S0304-3975(99)00118-8_BIB10","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1016\/0304-3975(94)00021-2","article-title":"Automatizing termination proofs of recursively defined functions","volume":"135(2)","author":"Manoury","year":"1994","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(99)00118-8_BIB11","doi-asserted-by":"crossref","unstructured":"P. Manoury, M. Parigot, M. Simonot, ProPre: a programming language with proofs, Proc. LPAR 92, Lecture Notes in Artificial Intelligence, vol. 624, 1992.","DOI":"10.1007\/BFb0013095"},{"key":"10.1016\/S0304-3975(99)00118-8_BIB12","unstructured":"F. Monin, Preuves de totalit\u00e9 de fonctions: mesures ordinales, application au syst\u00e8me de Boyer-Moore, Ph.D. Thesis, University of Savoie, 1995."},{"key":"10.1016\/S0304-3975(99)00118-8_BIB13","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1016\/0304-3975(92)90042-E","article-title":"Recursive programming with proofs","volume":"94(2)","author":"Parigot","year":"1992","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(99)00118-8_BIB14","series-title":"Recursive Functions","author":"P\u00e9ter","year":"1967"},{"key":"10.1016\/S0304-3975(99)00118-8_BIB15","doi-asserted-by":"crossref","unstructured":"A. Setzer, An introduction to well-ordering proofs in Martin-L\u00f6f's type theory, in: G. Sambin, J. Smith (Eds.), Twenty Five Years of Constructive Type Theory, Oxford University Press, Oxford, 1998.","DOI":"10.1016\/S0168-0072(97)00078-X"},{"key":"10.1016\/S0304-3975(99)00118-8_BIB16","doi-asserted-by":"crossref","unstructured":"K. Slind, Function definition in higher order logic, in: J. von Wright, J. Grundy, J. Harrison (Eds.), Proc. 9th Internat. Conf. on Theorem Proving in Higher Order Logics, TPHOLs\u201996, Lecture Notes in Computer Science, vol. 1125, Springer, Berlin, 1996.","DOI":"10.1007\/BFb0105417"},{"key":"10.1016\/S0304-3975(99)00118-8_BIB17","unstructured":"P. Weis et al., The CAML reference manual, version 2.61, Technical Report 121, INRIA, 1990."},{"key":"10.1016\/S0304-3975(99)00118-8_BIB18","doi-asserted-by":"crossref","unstructured":"P. Manoury, A User's friendly syntax to define recursive functions as typed lambda-terms, Proceedings of Type for proofs and programs TYPES\u201994, LIVCS, vol. 996, 1994.","DOI":"10.1007\/3-540-60579-7_5"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397599001188?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397599001188?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,1,15]],"date-time":"2020-01-15T17:22:07Z","timestamp":1579108927000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397599001188"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,3]]},"references-count":18,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2001,3]]}},"alternative-id":["S0304397599001188"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(99)00118-8","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2001,3]]}}}