Write a Blog >>
Mon 20 Jan 2020 15:35 - 15:56 at Maurepas - Decidability and complexity Chair(s): Kathrin Stark

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 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
CPP-2020-papers15:35 - 15:56
Yannick ForsterSaarland University, Fabian KunzeSaarland University, Maximilian WuttkeSaarland University
DOI Pre-print Media Attached
CPP-2020-papers15:56 - 16:18
Linh TranNational University of Singapore, Anshuman MohanNational University of Singapore, Aquinas HoborNational University of Singapore
DOI Pre-print Media Attached
CPP-2020-papers16:18 - 16:40
Simon SpiesSaarland University, Yannick ForsterSaarland University
DOI Pre-print Media Attached