Publication details

Saarland University Computer Science

Verification of PCP-Related Computational Reductions in Coq

Yannick Forster, Edith Heiter, Gert Smolka

arXiv:1711.07023, 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.

Coq Formalisation - arxiv publication

Download PDF        Show BibTeX               


Login to edit


Webmaster, Wed Sep 16 10:47:00 2009