Verified Programming of Turing Machines in Coq
We present a framework for the verified programming of multi-tape Turing machines in Coq. Improving on prior work by Asperti and Ricciotti in Matita, we implement multiple layers of abstraction. The highest layer allows a user to implement nontrivial algorithms as Turing machines and verify their correctness, as well as time and space complexity compositionally. The user can do so without ever mentioning states, symbols on tapes or transition functions: They write programs in an imperative language with registers containing values of encodable data types, and our framework constructs corresponding Turing machines.
As case studies, we verify a translation from multi-tape to single-tape machines as well as a universal Turing machine, both with polynomial time overhead and constant factor space overhead.
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
|Verified Programming of Turing Machines in Coq|
Yannick Forster Saarland University, Fabian Kunze Saarland University, Maximilian Wuttke Saarland UniversityDOI Pre-print Media Attached
|A Functional Proof Pearl: Inverting the Ackermann Hierarchy|
Linh Tran National University of Singapore, Anshuman Mohan National University of Singapore, Aquinas Hobor National University of SingaporeDOI Pre-print Media Attached
|Undecidability of Higher-Order Unification Formalised in Coq|
Simon Spies Saarland University, Yannick Forster Saarland UniversityDOI Pre-print Media Attached