Context-Free Grammars and Languages

Tobias Nipkow 📧, Markus Gschoßmann 📧, Felix Krayer 📧, Fabian Lehr 📧, Bruno Philipp 📧, August Martin Stimpfle, Kaan Taskin 📧 and Akihisa Yamada 📧

May 21, 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 is a basic library of definitions and results about context-free grammars and languages. It includes context-free grammars and languages, parse trees, Chomsky normal form, pumping lemmas and the relationship of right-linear grammars to finite automata.

License

BSD License

History

November 19, 2025
Made CNF translation contructive. Binarization proofs due to Felipe Escallon

Topics

Session Context_Free_Grammar

Depends on

Used by

Cite

× 
@article{Context_Free_Grammar-AFP,
  author  = {Tobias Nipkow and Markus Gschoßmann and Felix Krayer and Fabian Lehr and Bruno Philipp and August Martin Stimpfle and Kaan Taskin and Akihisa Yamada},
  title   = {Context-Free Grammars and Languages},
  journal = {Archive of Formal Proofs},
  month   = {May},
  year    = {2025},
  note    = {\url{https://isa-afp.org/entries/Context_Free_Grammar.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download