# Verification of PCP-Related Computational Reductions in Coq

arXiv: https://arxiv.org/abs/1711.07023 · HTML: https://mlsanity.com/paper/1711.07023/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 19 Nov 2017.

## Built on by (most cited first, 1 of 1)

- [Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens](https://mlsanity.com/paper/2104.14445/) (2021)

## Abstract (arXiv)

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.