Advisors: Yannick Forster, Gert Smolka
We study, formalize, and verify reductions of the halting problem for Turing machines (Halt) to the Post correspondence problem (PCP). The formalizations and verifications are carried out with the interactive theorem prover Coq with constructive proofs not using excluded middle. We verify 7 reductions: Halt to SR (word problem for string rewriting), SR to MPCP (Post correspondence problem with fixed first domino) and MPCP to PCP. We present an alternative, direct reduction of Halt to MPCP, and reductions of SR to RSR (word problem for string rewriting with nonempty rules) as well as RSR to PCP. In addition, the reduction of Halt to SR includes a reduction of the reachability problem for Turing machines (Reach) to SR. We observe that the correctness of the reductions is argued rather informally in the literature and that the formal verification requires considerable elaboration and effort.