From: Peter Lammich <lammich@in.tum.de>
I'm happy to announce the new entry Pushdown Automata, by Kaan Taskin
and Tobias Nipkow.
https://www.isa-afp.org/entries/Pushdown_Automata.html
Abstract
This entry formalizes pushdown automata and proves their equivalence
with context-free grammars. It also shows that acceptance by empty stack
and by final state are equivalent.
--
Peter
Last updated: Oct 20 2025 at 16:27 UTC