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 Jan Times are displayed in time zone: (GMT-06:00) Saskatchewan, Central America change

 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