Skip navigation
Skip navigation
The system will be down for maintenance between 8:00 and 8:15am on Wednesday 12, December 2018

Mechanisation of PDA and Grammar Equivalence for Context-Free Languages

Barthwal, Aditi; Norrish, Michael


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.

CollectionsANU Research Publications
Date published: 2010
Type: Conference paper
Source: WoLLIC 2010 proceedings
DOI: 10.1007/978-3-642-13824-9_11


File Description SizeFormat Image
01_Barthwal_Mechanisation_of_PDA_and_2010.pdf105.49 kBAdobe PDF    Request a copy

Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  27 November 2018/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator