@InProceedings{RMAMDN2018,
author="Ramos, Thiago Mendon{\c{c}}a Ferreira
and Mu{\~{n}}oz, C{\'e}sar
and Ayala-Rinc{\'o}n, Mauricio
and Moscato, Mariano
and Dutle, Aaron
and Narkawicz, Anthony",
editor="Moss, Lawrence S.
and de Queiroz, Ruy
and Martinez, Maricarmen",
title="Formalization of the Undecidability of the Halting Problem for a Functional Language",
booktitle="Logic, Language, Information, and Computation",
year="2018",
month="July",
publisher="Springer Berlin Heidelberg",
series = "Lecture Notes in Computer Science",      
volume = "10944",
address="Oxford, UK",
pages="196--209",
abstract="This paper presents a formalization of the proof of the undecidability of the halting problem for a functional programming language. The computational model consists of a simple first-order functional language called PVS0 whose operational semantics is specified in the Prototype Verification System (PVS). The formalization is part of a termination analysis library in PVS that includes the specification and equivalence proofs of several notions of termination. The proof of the undecidability of the halting problem required classical constructions such as mappings between naturals and PVS0 programs and inputs. These constructs are used to disprove the existence of a PVS0 program that decides termination of other programs, which gives rise to a contradiction.",
isbn="978-3-662-57669-4",
doi="10.1007/978-3-662-57669-4_11"
}