Constructive Many-one Reduction from the Halting Problem to Semi-unification (Extended Version)

DOI10.46298/lmcs-19(4:22)2023arXiv2208.13428MaRDI QIDQ6137845

Andrej Dudenhefner

Publication date: 16 January 2024

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2208.13428

zbMATH Keywords

undecidabilityconstructive mathematicscomputability theoryCoqsemi-unificationmechanization

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Cites Work

• A formalization of multi-tape Turing machines
• The undecidability of the semi-unification problem
• A theory of type polymorphism in programming
• Typability and type checking in System F are equivalent and undecidable
• Small universal register machines
• Counter machines
• Verification of PCP-related computational reductions in Coq
• The surveyability of mathematical proof: A historical perspective
• On Forward Closure and the Finite Variant Property
• On Immortal Configurations in Turing Machines
• Unification Modulo Synchronous Distributivity
• Periodicity and Immortality in Reversible Computing
• The Tiling Problem Revisited (Extended Abstract)
• An analysis of ML typability
• The undecidability of the Turing machine immortality problem
• A variant of a recursively unsolvable problem
• [https://portal.mardi4nfdi.de/wiki/Publication:5875425 A certifying extraction with time bounds from Coq to call-by-value $\lambda$-calculus]
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Constructive Many-one Reduction from the Halting Problem to Semi-unification (Extended Version)