{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T14:23:05Z","timestamp":1775053385922,"version":"3.50.1"},"reference-count":0,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2002,1,9]],"date-time":"2002-01-09T00:00:00Z","timestamp":1010534400000},"content-version":"unspecified","delay-in-days":8,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2002,1]]},"abstract":"<jats:p>We introduce a language based upon lambda calculus with products, coproducts and strictly \npositive inductive types that allows the definition of recursive terms. We present the \nimplementation (foetus) of a syntactical check that ensures that all such terms are structurally \nrecursive, i.e. recursive calls appear only with arguments structurally smaller than the input \nparameters of terms considered. To ensure the correctness of the termination checker, we \nshow that all structurally recursive terms are normalizing with respect to a given operational \nsemantics. To this end, we define a semantics on all types and a structural ordering on the \nvalues in this semantics and prove that all values are accessible with regard to this ordering. \nFinally, we point out how to do this proof predicatively using set based operators.<\/jats:p>","DOI":"10.1017\/s0956796801004191","type":"journal-article","created":{"date-parts":[[2008,8,8]],"date-time":"2008-08-08T14:02:48Z","timestamp":1218204168000},"page":"1-41","source":"Crossref","is-referenced-by-count":31,"title":["A predicative analysis of structural recursion"],"prefix":"10.1017","volume":"12","author":[{"given":"ANDREAS","family":"ABEL","sequence":"first","affiliation":[]},{"given":"THORSTEN","family":"ALTENKIRCH","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2002,1,9]]},"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796801004191","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,21]],"date-time":"2025-06-21T05:12:43Z","timestamp":1750482763000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796801004191\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,1]]},"references-count":0,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2002,1]]}},"alternative-id":["S0956796801004191"],"URL":"https:\/\/doi.org\/10.1017\/s0956796801004191","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2002,1]]}}}