{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:36:07Z","timestamp":1740123367394,"version":"3.37.3"},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2022,1,30]],"date-time":"2022-01-30T00:00:00Z","timestamp":1643500800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,30]],"date-time":"2022-01-30T00:00:00Z","timestamp":1643500800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100003593","name":"Conselho Nacional de Desenvolvimento Cient\u00edfico e Tecnol\u00f3gico","doi-asserted-by":"publisher","award":["307672\/2017-4"],"award-info":[{"award-number":["307672\/2017-4"]}],"id":[{"id":"10.13039\/501100003593","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002322","name":"Coordena\u00e7\u00e3o de Aperfei\u00e7oamento de Pessoal de N\u00edvel Superior","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100002322","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002322","name":"Coordena\u00e7\u00e3o de Aperfei\u00e7oamento de Pessoal de N\u00edvel Superior","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100002322","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2022,11]]},"DOI":"10.1007\/s10817-021-09615-x","type":"journal-article","created":{"date-parts":[[2022,1,30]],"date-time":"2022-01-30T00:03:06Z","timestamp":1643500986000},"page":"1031-1063","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Formalization of the Computational Theory of a Turing Complete Functional Language Model"],"prefix":"10.1007","volume":"66","author":[{"given":"Thiago Mendon\u00e7a Ferreira","family":"Ramos","sequence":"first","affiliation":[]},{"given":"Ariane Alves","family":"Almeida","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0089-3905","authenticated-orcid":false,"given":"Mauricio","family":"Ayala-Rinc\u00f3n","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,1,30]]},"reference":[{"doi-asserted-by":"publisher","unstructured":"Alves\u00a0Almeida, A., Ayala-Rincon, M.: Formalizing the dependency pair criterion for innermost termination. Sci. Comput. Program. 195, 102474 (2020). https:\/\/doi.org\/10.1016\/j.scico.2020.102474","key":"9615_CR1","DOI":"10.1016\/j.scico.2020.102474"},{"doi-asserted-by":"publisher","unstructured":"Arts, T.: Termination by absence of infinite chains of dependency pairs. In: 21st International Colloquium on Trees in Algebra and Programming CAAP, LNCS, vol. 1059, pp. 196\u2013210. Springer (1996). https:\/\/doi.org\/10.1007\/3-540-61064-2_38","key":"9615_CR2","DOI":"10.1007\/3-540-61064-2_38"},{"key":"9615_CR3","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, 133\u2013178 (2000). https:\/\/doi.org\/10.1016\/S0304-3975(99)00207-8","journal-title":"Theor. Comput. Sci."},{"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, Department of Mathematics, Universidade de Bras\u00edlia (2014). http:\/\/repositorio.unb.br\/handle\/10482\/18069 (in Portuguese)","key":"9615_CR4"},{"issue":"3","key":"9615_CR5","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1145\/828.1882","volume":"31","author":"RS Boyer","year":"1984","unstructured":"Boyer, R.S., Moore, J.S.: A Mechanical Proof of the Unsolvability of the Halting Problem. J. Assoc. Comput. Mach. 31(3), 441\u2013458 (1984). https:\/\/doi.org\/10.1145\/828.1882","journal-title":"J. Assoc. Comput. Mach."},{"doi-asserted-by":"publisher","unstructured":"Carneiro, M.: Formalizing Computability Theory via Partial Recursive Functions. In: 10th International Conference on Interactive Theorem Proving ITP, LIPIcs, vol. 141, pp. 12:1\u201312:17. Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik (2019). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2019.12","key":"9615_CR6","DOI":"10.4230\/LIPIcs.ITP.2019.12"},{"doi-asserted-by":"publisher","unstructured":"Ferreira\u00a0Ramos, T.M., Mu\u00f1oz, C.A., Ayala-Rinc\u00f3n, M., Moscato, M.M., Dutle, A., Narkawicz, A.: Formalization of the undecidability of the halting problem for a functional language. In: 25th International Workshop on Logic, Language, Information, and Computation WoLLIC, LNCS, vol. 10944, pp. 196\u2013209. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-662-57669-4_11","key":"9615_CR7","DOI":"10.1007\/978-3-662-57669-4_11"},{"doi-asserted-by":"publisher","unstructured":"Floyd, R.W., Beigel, R.: The Language of Machines: An Introduction to Computability and Formal Languages. W H Freeman & Co (1994). https:\/\/doi.org\/10.2307\/2275690","key":"9615_CR8","DOI":"10.2307\/2275690"},{"doi-asserted-by":"publisher","unstructured":"Forster, Y., Larchey-Wendling, D.: Certified undecidability of intuitionistic linear logic via binary stack machines and Minsky machines. In: 8th ACM SIGPLAN International Conference on Certified Programs and Proofs CPP, pp. 104\u2013117. ACM (2019). https:\/\/doi.org\/10.1145\/3293880.3294096","key":"9615_CR9","DOI":"10.1145\/3293880.3294096"},{"doi-asserted-by":"publisher","unstructured":"Forster, Y., Smolka, G.: Weak call-by-value Lambda calculus as a model of computation in Coq. In: 8th International Conference on Interactive Theorem Proving ITP, LNCS, vol. 10499, pp. 189\u2013206. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-66107-0_13","key":"9615_CR10","DOI":"10.1007\/978-3-319-66107-0_13"},{"doi-asserted-by":"publisher","unstructured":"Forster, Y., Heiter, E., Smolka, G.: Verification of PCP-related computational reductions in Coq. In: 9th International Conference on Interactive Theorem Proving ITP, LNCS, vol. 10895, pp. 253\u2013269. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-94821-8_15","key":"9615_CR11","DOI":"10.1007\/978-3-319-94821-8_15"},{"doi-asserted-by":"publisher","unstructured":"Forster, Y., Kirst, D., Smolka, G.: On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem. In: 8th ACM SIGPLAN International Conference on Certified Programs and Proofs CPP, pp. 38\u201351. ACM (2019). https:\/\/doi.org\/10.1145\/3293880.3294091","key":"9615_CR12","DOI":"10.1145\/3293880.3294091"},{"key":"9615_CR13","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","volume":"13","author":"WD Goldfarb","year":"1981","unstructured":"Goldfarb, W.D.: The undecidability of the second-order unification problem. Theor. Comput. Sci. 13, 225\u2013230 (1981). https:\/\/doi.org\/10.1016\/0304-3975(81)90040-2","journal-title":"Theor. Comput. Sci."},{"unstructured":"Heiter, E.: Undecidability of the Post Correspondence Problem. Master\u2019s thesis, Faculty of Mathematics and Computer Science, Saarland University (2014). https:\/\/www.ps.uni-saarland.de\/~heiter\/downloads\/PCP_Undecidability.pdf","key":"9615_CR14"},{"unstructured":"Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation, 3rd edn. Pearson (2008)","key":"9615_CR15"},{"doi-asserted-by":"publisher","unstructured":"Johannisson, K.: Formalizing the Halting Problem in a Constructive type theory. In: International Workshop on Types for Proofs and Programs TYPES, LNCS, vol. 2277, pp. 145\u2013159. Springer (2000). https:\/\/doi.org\/10.1007\/3-540-45842-5_10","key":"9615_CR16","DOI":"10.1007\/3-540-45842-5_10"},{"doi-asserted-by":"crossref","unstructured":"Kirst, D., Larchey-Wendling, D.: Trakhtenbrot\u2019s Theorem in Coq, A Constructive Approach to Finite Model Theory. CoRR arXiv:2004.07390 (2020)","key":"9615_CR17","DOI":"10.1007\/978-3-030-51054-1_5"},{"doi-asserted-by":"publisher","unstructured":"Larchey-Wendling, D.: Typing total recursive functions in Coq. In: 8th International Conference on Interactive Theorem Proving ITP, LNCS, vol. 10499, pp. 371\u2013388. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-66107-0_24","key":"9615_CR18","DOI":"10.1007\/978-3-319-66107-0_24"},{"doi-asserted-by":"publisher","unstructured":"Larchey-Wendling, D., Forster, Y.: Hilbert\u2019s Tenth Problem in Coq. In: 4th International Conference on Formal Structures for Computation and Deduction FSCD, LIPIcs, vol. 131, pp. 27:1\u201327:20. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2019). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2019.27","key":"9615_CR19","DOI":"10.4230\/LIPIcs.FSCD.2019.27"},{"doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1145\/360204.360210","key":"9615_CR20","DOI":"10.1145\/360204.360210"},{"doi-asserted-by":"publisher","unstructured":"Manolios, P., Vroon, D.: Termination analysis with calling context graphs. In: 18th International Conference on Computer Aided Verification CAV, LNCS, vol. 4144, pp. 401\u2013414. Springer (2006). https:\/\/doi.org\/10.1007\/11817963_36","key":"9615_CR21","DOI":"10.1007\/11817963_36"},{"unstructured":"Mu\u00f1oz, C.A., Ayala-Rinc\u00f3n, M., Moscato, M.M., Dutle, A.M., Narkawicz, A.J., Almeida, A.A., Avelar, A.B., M.\u00a0Ferreira\u00a0Ramos, T.: Formal verification of termination criteria for first-order recursive functions. In: 12th International Conference on Interactive Theorem Proving (ITP 2021), LIPIcs, vol. 193, pp. 27:1\u201327:17. Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik (2021). URL https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2021\/13922","key":"9615_CR22"},{"doi-asserted-by":"publisher","unstructured":"Norrish, M.: Mechanised computability theory. In: Second International Conference on Interactive Theorem Proving ITP, LNCS, vol. 6898, pp. 297\u2013311. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22863-6_22","key":"9615_CR23","DOI":"10.1007\/978-3-642-22863-6_22"},{"issue":"1","key":"9615_CR24","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2307\/2267170","volume":"12","author":"EL Post","year":"1947","unstructured":"Post, E.L.: Recursive unsolvability of a problem of Thue. J. Symb. Logic 12(1), 1\u201311 (1947). https:\/\/doi.org\/10.2307\/2267170","journal-title":"J. Symb. Logic"},{"doi-asserted-by":"publisher","unstructured":"Sipser, M.: Introduction to the Theory of Computation, 3rd edn. Cengage Learning (2012). https:\/\/doi.org\/10.1145\/230514.571645","key":"9615_CR25","DOI":"10.1145\/230514.571645"},{"doi-asserted-by":"publisher","unstructured":"Spies, S., Forster, Y.: Undecidability of higher-order unification formalised in Coq. In: 9th ACM SIGPLAN International Conference on Certified Programs and Proofs CPP, pp. 143\u2013157. ACM (2020). https:\/\/doi.org\/10.1145\/3372885.3373832","key":"9615_CR26","DOI":"10.1145\/3372885.3373832"},{"issue":"4","key":"9615_CR27","first-page":"569","volume":"70","author":"BA Trakhtenbrot","year":"1950","unstructured":"Trakhtenbrot, B.A.: The impossibility of an algorithm for the decidability problem on finite classes. Doklady Akademii Nauk SSSR 70(4), 569\u2013572 (1950)","journal-title":"Doklady Akademii Nauk SSSR"},{"issue":"4","key":"9615_CR28","doi-asserted-by":"publisher","first-page":"153","DOI":"10.2307\/2268280","volume":"2","author":"AM Turing","year":"1937","unstructured":"Turing, A.M.: Computability and $$\\lambda $$-definability. J. Symb. Logic 2(4), 153\u2013163 (1937). https:\/\/doi.org\/10.2307\/2268280","journal-title":"J. Symb. Logic"},{"unstructured":"Turing, A.M.: Checking a large routine. In: Campbell-Kelly, M. (ed.) The Early British Computer Conferences, pp. 70\u201372. MIT Press, Cambridge, MA, USA (1989). URL http:\/\/dl.acm.org\/citation.cfm?id=94938.94952","key":"9615_CR29"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-021-09615-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-021-09615-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-021-09615-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,5]],"date-time":"2022-11-05T11:12:27Z","timestamp":1667646747000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-021-09615-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,30]]},"references-count":29,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2022,11]]}},"alternative-id":["9615"],"URL":"https:\/\/doi.org\/10.1007\/s10817-021-09615-x","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2022,1,30]]},"assertion":[{"value":"30 May 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 November 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 January 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}