FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Verification of PCP-Related Computational Reductions in Coq

Authors: Yannick Forster, Edith Heiter and Gert Smolka

PapersPapers with AbstractsPrefaceAuthor IndexKeyword Index

Paper Information

Title:Verification of PCP-Related Computational Reductions in Coq
Authors:Yannick Forster, Edith Heiter and Gert Smolka
Proceedings:ITP Papers
Editors: Jeremy Avigad and Assia Mahboubi
Keywords:Post Correspondence Problem, String Rewriting, Context-free Grammars, Computational Reductions, Undecidability
Abstract:

ABSTRACT. We formally verify several computational reductions concerning the Post correspondence problem (PCP) using the proof assistant Coq. Our verification includes a reduction of the halting problem for Turing 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.

Pages:17
Talk:Jul 12 10:00 (Session 70C)
Paper: