Publication details

Programming Systems

Gert Smolka

Publications

Teaching

Software

Formalizations

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               

@CONFERENCE{ForsterEtAl:2017:PCP,
  title = {Verification of PCP-Related Computational Reductions in Coq},
  author = {Yannick Forster and Edith Heiter and Gert Smolka},
  year = {2018},
  month = {Jul},
  publisher = {Springer},
  booktitle = { Interactive Theorem Proving - 9th International Conference, ITP 2018, Oxford, UK, July 9-12, 2018},
  series = {LNCS 10895},
  pages = {253-269},
  note = {Preliminary version appeared as arXiv:1711.07023},
}

Login to edit