Verification of PCP-Related Computational Reductions in Coq

Abstract

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.

Cited by in corpus (7)

• Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory (Extended Version)
• Undecidability of $D_{<:}$ and Its Decidable Fragments
• Trakhtenbrot's Theorem in Coq, A Constructive Approach to Finite Model Theory
• A certifying extraction with time bounds from Coq to call-by-value $\lambda$-calculus
• Hilbert's Tenth Problem in Coq (Extended Version)
• Constructive Many-one Reduction from the Halting Problem to Semi-unification (Extended Version)
• Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens