A Verified Translation of Multitape Turing Machines into Singletape Turing Machines by Christian Dalvit and René Thiemann Nov 30