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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Barthwal, A., Norrish, M.: Verified, executable parsing. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 160–174. Springer, Heidelberg (2009)
Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and Computation. Addison-Wesley, Reading (1979)
Nipkow, T.: Verified lexical analysis. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol. 1479, pp. 1–15. Springer, Heidelberg (1998)
Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 28–32. Springer, Heidelberg (2008); See also the HOL website at http://hol.sourceforge.net
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Barthwal, A., Norrish, M. (2010). Mechanisation of PDA and Grammar Equivalence for Context-Free Languages. In: Dawar, A., de Queiroz, R. (eds) Logic, Language, Information and Computation. WoLLIC 2010. Lecture Notes in Computer Science(), vol 6188. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-13824-9_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-13824-9_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-13823-2
Online ISBN: 978-3-642-13824-9
eBook Packages: Computer ScienceComputer Science (R0)