Trustworthy Systems

Mechanisation of PDA and grammar equivalence for context-free languages

Authors

Aditi Barthwal and Michael Norrish

Australian National University

NICTA

Abstract

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 proofs, but also how intensive such a process can turn out to be. The proofs blow up in size in way difficult to predict from examining original textbook presentations. Even a meticulous text proof has “intuitive” leaps that need to be identified and formalised.

BibTeX Entry

  @inproceedings{Barthwal_Norrish_10,
    address          = {Brasília, Brazil},
    author           = {Barthwal, Aditi and Norrish, Michael},
    booktitle        = {17th Workshop on Logic, Language, Information and Computation },
    editor           = {{Anuj Dawar}},
    keywords         = {language theory, interactive theorem proving},
    month            = jul,
    pages            = {125--135},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/3847.pdf},
    publisher        = {Springer},
    title            = {Mechanisation of {PDA} and Grammar Equivalence for Context-Free Languages},
    year             = {2010}
  }

Download