{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:00:33Z","timestamp":1767927633875,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642323461","type":"print"},{"value":"9783642323478","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-32347-8_17","type":"book-chapter","created":{"date-parts":[[2012,8,10]],"date-time":"2012-08-10T11:33:54Z","timestamp":1344598434000},"page":"250-265","source":"Crossref","is-referenced-by-count":18,"title":["Stop When You Are Almost-Full"],"prefix":"10.1007","author":[{"given":"Dimitrios","family":"Vytiniotis","sequence":"first","affiliation":[]},{"given":"Thierry","family":"Coquand","sequence":"additional","affiliation":[]},{"given":"David","family":"Wahlstedt","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","unstructured":"Abel, A.: Termination and productivity checking with continuous types. In: Proceedings of the 6th International Conference on Typed Lambda Calculi and Applications, TLCA 2003, Valencia, Spain, pp. 1\u201315. Springer, Heidelberg (2003), \n                    \n                      http:\/\/dl.acm.org\/citation.cfm?id=1762348.1762349\n                    \n                    \n                  , ISBN: 3-540-40332-9"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/3-540-36377-7_1","volume-title":"The Essence of Computation","author":"A.M. Ben-Amram","year":"2002","unstructured":"Ben-Amram, A.M.: General Size-Change Termination and Lexicographic Descent. In: Mogensen, T.\u00c6., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol.\u00a02566, pp. 3\u201317. Springer, Heidelberg (2002)"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-540-24849-1_5","volume-title":"Types for Proofs and Programs","author":"S. Berghofer","year":"2004","unstructured":"Berghofer, S.: A Constructive Proof of Higman\u2019s Lemma in Isabelle. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol.\u00a03085, pp. 66\u201382. Springer, Heidelberg (2004)"},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"issue":"4","key":"17_CR5","first-page":"827","volume":"21","author":"F. Blanqui","year":"2011","unstructured":"Blanqui, F., Koprowski, A.: Color: a COQ library on well-founded rewrite relations and its application to the automated verification of termination certificates. MSCS\u00a021(4), 827\u2013859 (2011)","journal-title":"MSCS"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Bolingbroke, M., Jones, S.P., Vytiniotis, D.: Termination combinators forever. In: Proceedings of the 4th ACM Symposium of Haskell 2011, pp. 23\u201334. ACM (2011)","DOI":"10.1145\/2034675.2034680"},{"key":"17_CR7","first-page":"671","volume":"15","author":"A. Bove","year":"2005","unstructured":"Bove, A., Capretta, V.: Modelling general recursion in type theory. MSCS\u00a015, 671\u2013708 (2005)","journal-title":"MSCS"},{"key":"17_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-642-14052-5_15","volume-title":"Interactive Theorem Proving","author":"A. Chargu\u00e9raud","year":"2010","unstructured":"Chargu\u00e9raud, A.: The Optimal Fixed Point Combinator. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 195\u2013210. Springer, Heidelberg (2010)"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: Proceedings of PLDI 2006, pp. 415\u2013426. ACM (2006)","DOI":"10.1145\/1133981.1134029"},{"key":"17_CR10","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1006\/inco.1994.1034","volume":"110","author":"T. Coquand","year":"1994","unstructured":"Coquand, T.: An analysis of Ramsey\u2019s Theorem. Inf. Comput.\u00a0110, 297\u2013304 (1994)","journal-title":"Inf. Comput."},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-642-25379-9_11","volume-title":"Certified Programs and Proofs","author":"T. Coquand","year":"2011","unstructured":"Coquand, T., Siles, V.: A Decision Procedure for Regular Expression Equivalence in Type Theory. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol.\u00a07086, pp. 119\u2013134. Springer, Heidelberg (2011)"},{"issue":"1\/2","key":"17_CR12","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/s002000100065","volume":"12","author":"N. Dershowitz","year":"2001","unstructured":"Dershowitz, N., Lindenstrauss, N., Sagiv, Y., Serebrenik, A.: A general framework for automatic termination analysis of logic programs. Appl. Algebra Eng. Commun. Comput.\u00a012(1\/2), 117\u2013156 (2001)","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/BFb0097789","volume-title":"Types for Proofs and Programs","author":"D. Fridlender","year":"1998","unstructured":"Fridlender, D.: Higman\u2019s Lemma in Type Theory. In: Gim\u00e9nez, E. (ed.) TYPES 1996. LNCS, vol.\u00a01512, pp. 112\u2013133. Springer, Heidelberg (1998)"},{"key":"17_CR14","unstructured":"Geser, A.: Relative termination. PhD thesis, Universit\u00e4t Passau (1990)"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-642-15769-1_4","volume-title":"Static Analysis","author":"M. Heizmann","year":"2010","unstructured":"Heizmann, M., Jones, N.D., Podelski, A.: Size-Change Termination and Transition Invariants. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol.\u00a06337, pp. 22\u201350. Springer, Heidelberg (2010)"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Jones, N.D., Bohr, N.: Call-by-value termination in the untyped lambda-calculus. Logical Methods in Computer Science\u00a04(1) (2008)","DOI":"10.2168\/LMCS-4(1:3)2008"},{"key":"17_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-642-22863-6_13","volume-title":"Interactive Theorem Proving","author":"A. Krauss","year":"2011","unstructured":"Krauss, A., Sternagel, C., Thiemann, R., Fuhs, C., Giesl, J.: Termination of Isabelle Functions via Termination of Rewriting. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol.\u00a06898, pp. 152\u2013167. Springer, Heidelberg (2011)"},{"key":"17_CR18","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/978-3-540-73595-3_34","volume-title":"Automated Deduction \u2013 CADE-21","author":"A. Krauss","year":"2007","unstructured":"Krauss, A.: Certified Size-Change Termination. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 460\u2013475. Springer, Heidelberg (2007)"},{"key":"17_CR19","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/s10817-009-9157-2","volume":"44","author":"A. Krauss","year":"2010","unstructured":"Krauss, A.: Partial and nested recursive function definitions in higher-order logic. Journal of Automated Reasoning\u00a044, 303\u2013336 (2010)","journal-title":"Journal of Automated Reasoning"},{"key":"17_CR20","first-page":"210","volume":"95","author":"J.B. Kruskal","year":"1960","unstructured":"Kruskal, J.B.: Well-quasi-ordering, the Tree Theorem, and Vazsonyi\u2019s conjecture. Trans. Amer. Math. Soc.\u00a095, 210\u2013225 (1960)","journal-title":"Trans. Amer. Math. Soc."},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: Proceedings of POPL 2001, pp. 81\u201392. ACM (2001)","DOI":"10.1145\/373243.360210"},{"key":"17_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/3-540-36377-7_17","volume-title":"The Essence of Computation","author":"M. Leuschel","year":"2002","unstructured":"Leuschel, M.: Homeomorphic Embedding for Online Termination of Symbolic Methods. In: Mogensen, T.\u00c6., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol.\u00a02566, pp. 379\u2013403. Springer, Heidelberg (2002)"},{"key":"17_CR23","doi-asserted-by":"crossref","unstructured":"Megacz, A.: A coinductive monad for Prop-bounded recursion. In: Stump, A., Xi, H. (eds.) Proceedings of PLPV 2007, pp. 11\u201320. ACM (2007)","DOI":"10.1145\/1292597.1292601"},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"Bezem, M.A., Nakata, K., Uustalu, T.: On streams that are finitely red. To appear in Logical Methods in Computer Science (2011)","DOI":"10.2168\/LMCS-8(4:4)2012"},{"key":"17_CR25","doi-asserted-by":"crossref","unstructured":"Nash-Williams, C.S.J.A.: On well-quasi-ordering finite trees. In: Mathematical Proceedings of the Cambridge Philosophical Society, vol.\u00a059, pp. 833\u2013835. Cambridge Univ. Press (1963)","DOI":"10.1017\/S0305004100003844"},{"key":"17_CR26","first-page":"32","volume-title":"Proceedings of LICS 2004","author":"A. Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: Proceedings of LICS 2004, pp. 32\u201341. IEEE Computer Society, Washington, DC (2004)"},{"key":"17_CR27","doi-asserted-by":"crossref","unstructured":"Richman, F., Stolzenberg, G.: Well-quasi-ordered sets. Advanced Mathematics, 145\u2013193 (1993)","DOI":"10.1006\/aima.1993.1004"},{"key":"17_CR28","unstructured":"Sagiv, Y.: A termination test for logic programs. In: ISLP, pp. 518\u2013532 (1991)"},{"key":"17_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/3-540-45842-5_15","volume-title":"Types for Proofs and Programs","author":"M. Seisenberger","year":"2002","unstructured":"Seisenberger, M.: An Inductive Version of Nash-Williams\u2019 Minimal-Bad-Sequence Argument for Higman\u2019s Lemma. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol.\u00a02277, pp. 233\u2013242. Springer, Heidelberg (2002)"},{"key":"17_CR30","doi-asserted-by":"crossref","unstructured":"Sereni, D.: Termination analysis and call graph construction for higher-order functional programs. In: Proceedings of ICFP 2007, pp. 71\u201384. ACM (2007)","DOI":"10.1145\/1291151.1291165"},{"key":"17_CR31","unstructured":"S\u00f8rensen, M.H., Gl\u00fcck, R.: An algorithm of generalization in positive supercompilation. In: Proceedings of ILPS 1995, The International Logic Programming Symposium, pp. 465\u2013479. MIT Press (1995)"},{"key":"17_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-540-74464-1_16","volume-title":"Types for Proofs and Programs","author":"M. Sozeau","year":"2007","unstructured":"Sozeau, M.: Subset Coercions in COQ. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol.\u00a04502, pp. 237\u2013252. Springer, Heidelberg (2007)"},{"issue":"1","key":"17_CR33","first-page":"41","volume":"2","author":"M. Sozeau","year":"2009","unstructured":"Sozeau, M.: A New Look at Generalized Rewriting in Type Theory. Journal of Formalized Reasoning\u00a02(1), 41\u201362 (2009)","journal-title":"Journal of Formalized Reasoning"},{"key":"17_CR34","unstructured":"Terese: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol.\u00a055. Cambridge University Press (2003)"},{"issue":"2","key":"17_CR35","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1112\/jlms\/s2-47.2.193","volume":"s2-47","author":"W. Veldman","year":"1993","unstructured":"Veldman, W., Bezem, M.: Ramsey\u2019s theorem and the pigeonhole principle in intuitionistic mathematics. Journal of the London Mathematical Society\u00a0s2-47(2), 193\u2013211 (1993)","journal-title":"Journal of the London Mathematical Society"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-32347-8_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T12:01:05Z","timestamp":1620129665000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-32347-8_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642323461","9783642323478"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-32347-8_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}