Pushdown Automata

Kaan Taskin 📧 and Tobias Nipkow 📧

October 15, 2025

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.

License

BSD License

Topics

Session Pushdown_Automata

Depends on

Cite

× 
@article{Pushdown_Automata-AFP,
  author  = {Kaan Taskin and Tobias Nipkow},
  title   = {Pushdown Automata},
  journal = {Archive of Formal Proofs},
  month   = {October},
  year    = {2025},
  note    = {\url{https://isa-afp.org/entries/Pushdown_Automata.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download