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

DOI10.1007/978-3-662-52921-8_21zbMath1478.68133OpenAlexW2489139193MaRDI 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 lemmaCoqformalizationChomsky normal formcontext-free language theorygrammar simplificationlanguage closure

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Grammars and rewriting systems (68Q42) Formalization of mathematics in connection with theorem provers (68V20)

Related Items (1)

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

This page was built for publication: On the Formalization of Some Results of Context-Free Language Theory