Verification of PCP-related computational reductions in Coq
scientific article; zbMATH DE number 6946984