{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T15:38:38Z","timestamp":1725982718482},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662576687"},{"type":"electronic","value":"9783662576694"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-662-57669-4_11","type":"book-chapter","created":{"date-parts":[[2018,6,26]],"date-time":"2018-06-26T08:48:51Z","timestamp":1530002931000},"page":"196-209","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Formalization of the Undecidability of the Halting Problem for a Functional Language"],"prefix":"10.1007","author":[{"given":"Thiago Mendon\u00e7a Ferreira","family":"Ramos","sequence":"first","affiliation":[]},{"given":"C\u00e9sar","family":"Mu\u00f1oz","sequence":"additional","affiliation":[]},{"given":"Mauricio","family":"Ayala-Rinc\u00f3n","sequence":"additional","affiliation":[]},{"given":"Mariano","family":"Moscato","sequence":"additional","affiliation":[]},{"given":"Aaron","family":"Dutle","sequence":"additional","affiliation":[]},{"given":"Anthony","family":"Narkawicz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,6,27]]},"reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/3-540-61064-2_38","volume-title":"Trees in Algebra and Programming \u2014 CAAP \u201996","author":"T Arts","year":"1996","unstructured":"Arts, T.: Termination by absence of infinite chains of dependency pairs. In: Kirchner, H. (ed.) CAAP 1996. LNCS, vol. 1059, pp. 196\u2013210. Springer, Heidelberg (1996). \nhttps:\/\/doi.org\/10.1007\/3-540-61064-2_38"},{"issue":"1\u20132","key":"11_CR2","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/S0304-3975(99)00207-8","volume":"236","author":"T Arts","year":"2000","unstructured":"Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236(1\u20132), 133\u2013178 (2000)","journal-title":"Theor. Comput. Sci."},{"key":"11_CR3","unstructured":"Avelar, A.B.: Formaliza\u00e7\u00e3o da automa\u00e7\u00e3o da termina\u00e7\u00e3o atrav\u00e9s de grafos com matrizes de medida. Ph.D. thesis, Universidade de Bras\u00edlia, Departamento de Matem\u00e1tica, Bras\u00edlia, Distrito Federal, Brasil (2015). In Portuguese"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-319-66107-0_13","volume-title":"Interactive Theorem Proving","author":"Y Forster","year":"2017","unstructured":"Forster, Y., Smolka, G.: Weak call-by-value lambda calculus as a model of computation in Coq. In: Ayala-Rinc\u00f3n, M., Mu\u00f1oz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 189\u2013206. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-66107-0_13"},{"key":"11_CR5","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. 6898, pp. 152\u2013167. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-22863-6_13"},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/978-3-319-66107-0_24","volume-title":"Interactive Theorem Proving","author":"D Larchey-Wendling","year":"2017","unstructured":"Larchey-Wendling, D.: Typing total recursive functions in Coq. In: Ayala-Rinc\u00f3n, M., Mu\u00f1oz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 371\u2013388. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-66107-0_24"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 81\u201392 (2001)","DOI":"10.1145\/360204.360210"},{"key":"11_CR8","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. 4144, pp. 401\u2013414. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/11817963_36"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/978-3-642-22863-6_22","volume-title":"Interactive Theorem Proving","author":"M Norrish","year":"2011","unstructured":"Norrish, M.: Mechanised computability theory. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 297\u2013311. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-22863-6_22"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction\u2014CADE-11","author":"S Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748\u2013752. Springer, Heidelberg (1992). \nhttps:\/\/doi.org\/10.1007\/3-540-55602-8_217"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1007\/3-540-44881-0_19","volume-title":"Rewriting Techniques and Applications","author":"R Thiemann","year":"2003","unstructured":"Thiemann, R., Giesl, J.: Size-change termination for term rewriting. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 264\u2013278. Springer, Heidelberg (2003). \nhttps:\/\/doi.org\/10.1007\/3-540-44881-0_19"},{"issue":"1","key":"11_CR12","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1112\/plms\/s2-42.1.230","volume":"42","author":"AM Turing","year":"1937","unstructured":"Turing, A.M.: On computable numbers, with an application to the Entscheidungsproblem. Proc. London Math. Soc. 42(1), 230\u2013265 (1937)","journal-title":"Proc. London Math. Soc."},{"key":"11_CR13","unstructured":"Turing, A.M.: Checking a large routine. In: Campbell-Kelly, M. (ed.) The Early British Computer Conferences, pp. 70\u201372. MIT Press, Cambridge (1989)"},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-642-39634-2_13","volume-title":"Interactive Theorem Proving","author":"J Xu","year":"2013","unstructured":"Xu, J., Zhang, X., Urban, C.: Mechanising Turing machines and computability theory in Isabelle\/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 147\u2013162. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-39634-2_13"},{"key":"11_CR15","unstructured":"Yamada, A., Sternagel, C., Thiemann, R., Kusakari, K.: AC dependency pairs revisited. In: Proceedings 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, LIPIcs, vol. 62, pp. 8:1\u20138:16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016)"}],"container-title":["Lecture Notes in Computer Science","Logic, Language, Information, and Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-57669-4_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,6,26]],"date-time":"2018-06-26T08:55:09Z","timestamp":1530003309000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-57669-4_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783662576687","9783662576694"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-57669-4_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}