Publication details

Saarland University Computer Science

Verification of PCP-Related Computational Reductions in Coq

Yannick Forster, Edith Heiter, Gert Smolka

submitted for review, 2017

We formally verify several computational reductions concerning the Post correspondence problem (PCP) using the proof assistant Coq. Our verifications include a reduction of a string rewriting problem generalising the halting problem for Turing machines to PCP, and reductions of PCP to the intersection problem and the palindrome problem for context-free grammars. Interestingly, rigorous correctness proofs for some of the reductions are missing in the literature.

Link to Coq Formalisation

Download PDF        Show BibTeX               


Login to edit


Webmaster, Wed Sep 16 10:47:00 2009