# Publication details

##
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

@ARTICLE{ForsterEtAl:2017:PCP,
title = {Verification of PCP-Related Computational Reductions in Coq},
author = {Yannick Forster and Edith Heiter and Gert Smolka},
year = {2017},
note = {submitted for review},
}

Login to edit

Webmaster,
Wed Sep 16 10:47:00 2009