Mon 20 Jan 2020 16:18 - 16:40 at Maurepas - Decidability and complexity Chair(s): Kathrin Stark

We formalise undecidability results concerning higher-order unification in the simply-typed $\lambda$-calculus with $\beta$-conversion in Coq. We prove the undecidability of general higher-order unification by reduction from Hilbert’s tenth problem, the solvability of Diophantine equations, following a proof by Dowek. We sharpen the result by establishing the undecidability of second-order and third-order unification following proofs by Goldfarb and Huet, respectively.

Goldfarb’s proof for second-order unification is by reduction from Hilbert’s tenth problem. Huet’s original proof uses the Post correspondence problem (PCP) to show the undecidability of third-order unification. We simplify and formalise his proof as a reduction from modified PCP. We also verify a decision procedure for first-order unification.

All proofs are carried out in the setting of synthetic undecidability and rely on Coq’s built-in notion of computation.

#### Mon 20 Jan

 15:35 - 16:40: CPP 2020 - Decidability and complexity at Maurepas Chair(s): Kathrin StarkSaarland University, Germany 15:35 - 15:56Talk Verified Programming of Turing Machines in CoqYannick ForsterSaarland University, Fabian KunzeSaarland University, Maximilian WuttkeSaarland University DOI Pre-print Media Attached 15:56 - 16:18Talk A Functional Proof Pearl: Inverting the Ackermann HierarchyLinh TranNational University of Singapore, Anshuman MohanNational University of Singapore, Aquinas HoborNational University of Singapore DOI Pre-print Media Attached 16:18 - 16:40Talk Undecidability of Higher-Order Unification Formalised in CoqSimon SpiesSaarland University, Yannick ForsterSaarland University DOI Pre-print Media Attached