{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:01:04Z","timestamp":1725490864354},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540735946"},{"type":"electronic","value":"9783540735953"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73595-3_34","type":"book-chapter","created":{"date-parts":[[2007,8,30]],"date-time":"2007-08-30T09:31:33Z","timestamp":1188466293000},"page":"460-475","source":"Crossref","is-referenced-by-count":18,"title":["Certified Size-Change Termination"],"prefix":"10.1007","author":[{"given":"Alexander","family":"Krauss","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"34_CR1","unstructured":"Archive of Formal Proofs. \n                    \n                      http:\/\/afp.sourceforge.net\/"},{"key":"34_CR2","unstructured":"Termination Competition. \n                    \n                      http:\/\/www.lri.fr\/~marche\/termination-competition\/"},{"key":"34_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/3-540-45842-5_2","volume-title":"Types for Proofs and Programs","author":"S. Berghofer","year":"2002","unstructured":"Berghofer, S., Nipkow, T.: Executing higher order logic. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol.\u00a02277, pp. 24\u201340. Springer, Heidelberg (2002)"},{"key":"34_CR4","volume-title":"Texts in theoretical comp. science","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive theorem proving and program development: Coq\u2019Art: the calculus of inductive constructions. In: Texts in theoretical comp. science, Springer, Heidelberg (2004)"},{"key":"34_CR5","unstructured":"Blanqui, F., Coupet-Grimal, S., Delobel, W., Hinderer, S., Koprowski, A.: CoLoR, a Coq library on rewriting and termination. In: Geser, A., S\u00f8ndergaard, H. (eds.) Eighth International Workshop on Termination, WST 2006, Seattle, WA, USA (2006)"},{"key":"34_CR6","doi-asserted-by":"crossref","unstructured":"Bulwahn, L., Krauss, A., Nipkow, T.: Finding Lexicographic Orders for Termination Proofs in Isabelle\/HOL. TPHOLs 2007 (to appear, 2007)","DOI":"10.1007\/978-3-540-74591-4_5"},{"key":"34_CR7","volume-title":"Introduction to HOL: A theorem proving environment for higher order logic","author":"M. Gordon","year":"1993","unstructured":"Gordon, M., Melham, T.: Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, Cambridge (1993)"},{"key":"34_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1007\/11541868_7","volume-title":"Theorem Proving in Higher Order Logics","author":"B. Gr\u00e9goire","year":"2005","unstructured":"Gr\u00e9goire, B., Mahboubi, A.: Proving equalities in a commutative ring done right in Coq. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 98\u2013113. Springer, Heidelberg (2005)"},{"key":"34_CR9","unstructured":"Haftmann, F., Nipkow, T.: A design for a generic code generator for the Isabelle\/HOL system, Manuscript (2007)"},{"key":"34_CR10","unstructured":"Harrison, J.: The HOL Light theorem prover. \n                    \n                      http:\/\/www.cl.cam.ac.uk\/users\/jrh\/hol-light"},{"key":"34_CR11","volume-title":"Computer-Aided Reasoning: An Approach","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Boston (2000)"},{"key":"34_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/BFb0029594","volume-title":"Mathematical Foundations of Computer Science 1990","author":"D. Kozen","year":"1990","unstructured":"Kozen, D.: On Kleene algebras and closed semirings. In: Rovan, B. (ed.) Mathematical Foundations of Computer Science 1990. LNCS, vol.\u00a0452, pp. 26\u201347. Springer, Heidelberg (1990)"},{"key":"34_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/11814771_48","volume-title":"Automated Reasoning","author":"A. Krauss","year":"2006","unstructured":"Krauss, A.: Partial recursive functions in higher-order logic. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 589\u2013603. Springer, Heidelberg (2006)"},{"key":"34_CR14","doi-asserted-by":"crossref","unstructured":"Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: ACM Symposium on Principles of Prog. Languages, pp. 81\u201392 (2001)","DOI":"10.1145\/360204.360210"},{"key":"34_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/11817963_36","volume-title":"Computer Aided Verification","author":"P. Manolios","year":"2006","unstructured":"Manolios, P., Vroon, D.: Termination analysis with calling context graphs. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 401\u2013414. Springer, Heidelberg (2006)"},{"key":"34_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"34_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) Automated Deduction - CADE-11. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"34_CR18","volume-title":"Computational Complexity","author":"C.H. Papadimitriou","year":"1994","unstructured":"Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, New York (1994)"},{"key":"34_CR19","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"398","DOI":"10.1007\/978-3-540-32275-7_26","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"N. Schirmer","year":"2005","unstructured":"Schirmer, N.: A verification environment for sequential imperative programs in Isabelle\/HOL. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, pp. 398\u2013414. Springer, Heidelberg (2005)"},{"key":"34_CR20","unstructured":"Wenzel, M.: Using axiomatic type classes in Isabelle, Isabelle documentation (2000)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-21"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73595-3_34.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T09:53:09Z","timestamp":1619517189000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73595-3_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540735946","9783540735953"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73595-3_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}