Publication details

Saarland University Computer Science

Verification of PCP-Related Computational Reductions in Coq

Yannick Forster, Edith Heiter, Gert Smolka

Interactive Theorem Proving - 9th International Conference, ITP 2018, Oxford, UK, July 9-12, 2018, 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