A mechanisation of some context-free language theory in HOL4

DOI10.1016/j.jcss.2013.05.003zbMath1433.68531OpenAlexW2005008302MaRDI QIDQ386032

Michael Norrish, Aditi Barthwal

Publication date: 13 December 2013

Published in: Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jcss.2013.05.003

zbMATH Keywords

context-free grammarsclosure propertiescontext-free languagespushdown automataHOL4

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

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

Uses Software

• Coq
• HOL
• TRX

Cites Work

• Unnamed Item
• Unnamed Item
• Simple, Functional, Sound and Complete Parsing for All Context-Free Grammars
• A Brief Overview of HOL4
• TRX: A Formally Verified Parser Interpreter
• A Formalisation of the Normal Forms of Context-Free Grammars in HOL4
• Verified, Executable Parsing
• Total parser combinators

This page was built for publication: A mechanisation of some context-free language theory in HOL4