Sciweavers

WOLLIC
2010
Springer
13 years 2 months ago
Mechanisation of PDA and Grammar Equivalence for Context-Free Languages
We provide a formalisation of the theory of pushdown automata (PDAs) using the HOL4 theorem prover. It illustrates how provers such as HOL can be used for mechanising complicated p...
Aditi Barthwal, Michael Norrish