Publication details

Saarland University Computer Science

Verification of PCP-Related Computational Reductions in Coq

Yannick Forster, Edith Heiter, Gert Smolka

Interactive Theorem proving (ITP 2018), Oxford, pp. 253-269, Springer, July 2018

We formally verify several computational reductions con- cerning the Post correspondence problem (PCP) using the proof assistant Coq. Our verification includes a reduction of the halting problem for Tur- ing machines to string rewriting, a reduction of string rewriting to PCP, and reductions of PCP to the intersection problem and the palindrome problem for context-free grammars.

Coq Formalisation - Preliminary version at arXiv

Download PDF        Show BibTeX               


Login to edit


Legal notice, Privacy policy