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

We implement in Gallina a hierarchy of functions that calculate the upper inverses to the hyperoperation/Ackermann hierarchy. Our functions run in $\Theta(b)$ for inputs expressed in unary, and in $O(b^2)$ for inputs expressed in binary (where $b$ = bitlength). We use our inverses to define linear-time functions—$\Theta(b)$ for both unary-represented and binary-represented inputs—that compute the upper inverse of the diagonal Ackermann function $\mathcal{A}(n)$. We show that these functions are consistent with the usual definition of the inverse Ackermann function $\alpha(n)$.

#### Mon 20 JanDisplayed time zone: Saskatchewan, Central America change

 15:35 - 16:40 Decidability and complexityCPP at Maurepas Chair(s): Kathrin Stark Princeton University, USA 15:3521mTalk Verified Programming of Turing Machines in CoqCPPYannick Forster Saarland University, Fabian Kunze Saarland University, Maximilian Wuttke Saarland University DOI Pre-print Media Attached 15:5621mTalk A Functional Proof Pearl: Inverting the Ackermann HierarchyCPPLinh Tran National University of Singapore, Anshuman Mohan National University of Singapore, Aquinas Hobor National University of Singapore DOI Pre-print Media Attached 16:1821mTalk Undecidability of Higher-Order Unification Formalised in CoqCPPSimon Spies Saarland University, Yannick Forster Saarland University DOI Pre-print Media Attached