Context-Free Grammars and Languages. - Tobias Nipkow; Markus Gschoßmann; Felix Krayer; Fabian Lehr; Bruno Philipp; August Martin Stimpfle; Kaan Taskin; Akihisa Yamada 002 (Arch. Formal Proofs, 2025)