On the Formalization of Some Results of Context-Free Language Theory

DOI10.1007/978-3-662-52921-8_21zbMath1478.68133MaRDI QIDQ2820703

Marcus V. M. Ramos, Ruy J. G. B. de Queiroz, Nelma Moreira, José Bacelar Almeida

Publication date: 9 September 2016

Published in: Logic, Language, Information, and Computation (Search for Journal in Brave)

Full work available at URL: http://repositorio.inesctec.pt/handle/123456789/4753

zbMATH Keywords

pumping lemma; Coq; formalization; Chomsky normal form; context-free language theory; grammar simplification; language closure

Mathematics Subject Classification ID

68Q45: Formal languages and automata

68Q42: Grammars and rewriting systems

68V20: Formalization of mathematics in connection with theorem provers

Related Items

Some applications of the formalization of the pumping lemma for context-free languages

Uses Software

• Coq
• TRX
• GitHub

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A mechanisation of some context-free language theory in HOL4
• Certified CYK parsing of context-free languages
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Validating LR(1) Parsers
• A Constructive Theory of Regular Languages in Coq
• Simple, Functional, Sound and Complete Parsing for All Context-Free Grammars
• On certain formal properties of grammars
• TRX: A Formally Verified Parser Interpreter
• A Formalisation of the Normal Forms of Context-Free Grammars in HOL4
• Mechanisation of PDA and Grammar Equivalence for Context-Free Languages