Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Multitape TMs


view this post on Zulip Email Gateway (Aug 26 2026 at 06:37):

From: Tobias Nipkow <nipkow@in.tum.de>

András Z. Salamon and Michael Wehar have given us a large chunk of multitape
Turing machine theory in the form of these four entries:

https://isa-afp.org/entries/Multitape_TM_Substrate.html
https://isa-afp.org/entries/Multitape_Alphabet_Reduction.html
https://isa-afp.org/entries/Multitape_Alphabet_Enlargement.html
https://isa-afp.org/entries/Multitape_Alphabet_Roundtrip.html

If you ever wondered whether some TM construction in Hopcroft and Ullman really
works, look no further.

Enjoy!

smime.p7s


Last updated: Sep 02 2026 at 16:10 UTC