Pushdown Automata

Kaan Taskin 📧 and Tobias Nipkow 📧

October 15, 2025

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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