zbMATH — the first resource for mathematics

On the formalization of some results of context-free language theory. (English) Zbl 06625896
Väänänen, Jouko (ed.) et al., Logic, language, information, and computation. 23rd international workshop, WoLLIC 2016, Puebla, Mexico, August 16–19th, 2016. Proceedings. Berlin: Springer (ISBN 978-3-662-52920-1/pbk; 978-3-662-52921-8/ebook). Lecture Notes in Computer Science 9803, 338-357 (2016).
Summary: This work describes a formalization effort, using the Coq proof assistant, of fundamental results related to the classical theory of context-free grammars and languages. These include closure properties (union, concatenation and Kleene star), grammar simplification (elimination of useless symbols, inaccessible symbols, empty rules and unit rules), the existence of a Chomsky normal form for context-free grammars and the Pumping lemma for context-free languages. The result is an important set of libraries covering the main results of context-free language theory, with more than 500 lemmas and theorems fully proved and checked. This is probably the most comprehensive formalization of the classical context-free language theory in the Coq proof assistant done to the present date, and includes the important result that is the formalization of the Pumping lemma for context-free languages.
For the entire collection see [Zbl 1343.03002].

03B70 Logic in computer science
Coq; GitHub; TRX
Full Text: DOI
[1] Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Springer, Heidelberg (2004) · Zbl 1069.68095 · doi:10.1007/978-3-662-07964-5
[2] Sudkamp, T.A.: Languages and Machines, 3rd edn. Addison-Wesley, Redwood City (2006)
[3] Ramos, M.V.M., Neto, J.J., Vega, I.S.: Linguagens Formais: Teoria Modelagem e Implementação. Bookman, Brisbane (2009)
[4] Ramos, M.V.M.: Formalization of Context-Free Language Theory. Ph.D. thesis, Centro de Informática-UFPE (2016). www.univasf.edu.br/ marcus.ramos/tese.pdf . Accessed 5 May 2016
[5] Ramos, M.V.M.: Source files of [4] (2016). https://github.com/mvmramos/v1 . Accessed 3 May 2016
[6] Chomsky, A.N.: On certain formal properties of grammar. Inf. Control 2, 137–167 (1959) · Zbl 0088.10801 · doi:10.1016/S0019-9958(59)90362-6
[7] Bar-Hillel, Y.: Language and Information: Selected Essays on Their Theory and Application. Addison-Wesley Series in Logic. Addison-Wesley Publishing Co., Redwood City (1964) · Zbl 0158.24102
[8] Hopcroft, J.E., Ullman, J.D.: Formal Languages and Their Relation to Automata. Addison-Wesley Longman Publishing Co., Inc., Boston (1969) · Zbl 0196.01701
[9] Davis, M.D., Sigal, R., Weyuker, E.J.: Computability, Complexity, and Languages: Fundamentals of Theoretical Computer Science, 2nd edn. Academic Press Professional Inc., San Diego (1994)
[10] Kozen, D.C.: Automata and Computability. Springer, Heidelberg (1997) · Zbl 0883.68055 · doi:10.1007/978-1-4612-1844-9
[11] Hopcroft, J.E., Motwani, R., Rotwani, Ullman, J.D.: Introduction to Automata Theory, Languages and Computability, 2nd edn. Addison-Wesley Longman Publishing Co., Inc., Boston (2000)
[12] Ginsburg, S.: The Mathematical Theory of Context-Free Languages. McGraw-Hill Inc., New York (1966) · Zbl 0184.28401
[13] Denning, P.J., Dennis, J.B., Qualitz, J.E.: Machines, Languages and Computation. Prentice-Hall, Upper Saddle River (1978) · Zbl 0492.68003
[14] Brookshear, J.G.: Theory of Computation: Formal Languages, Automata, and Complexity. Benjamin-Cummings Publishing Co., Inc., Redwood City (1989) · Zbl 0678.68001
[15] Lewis, H.R., Papadimitriou, C.H.: Elements of the Theory of Computation, 2nd edn. Prentice Hall PTR, Upper Saddle River (1998)
[16] Sipser, M.: Introduction to the Theory of Computation, 2nd edn. International Thomson Publishing, Toronto (2005) · Zbl 1169.68300
[17] Harrison, M.A.: Introduction to Formal Language Theory, 1st edn. Addison-Wesley Longman Publishing Co., Inc., Boston (1978) · Zbl 0411.68058
[18] Amarilli, A., Jeanmougin, M.: A proof of the pumping lemma for context-free languages through pushdown automata. CoRR abs/1207.2819 (2012)
[19] INRIA: Coq users’ contributions (2015). http://www.lix.polytechnique.fr/coq/pylons/contribs/index . Accessed 26 Oct 2015
[20] Koprowski, A., Binsztok, H.: TRX: a formally verified parser interpreter. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 345–365. Springer, Heidelberg (2010). http://dx.doi.org/10.1007/978-3-642-11957-6_19 . Accessed 26 Oct 2015 · Zbl 1260.68194 · doi:10.1007/978-3-642-11957-6_19
[21] Ridge, T.: Simple, functional, sound and complete parsing for all context-free grammars. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 103–118. Springer, Heidelberg (2011) · Zbl 1350.68164 · doi:10.1007/978-3-642-25379-9_10
[22] Jourdan, J.-H., Pottier, F., Leroy, X.: Validating LR(1) parsers. In: Seidl, H. (ed.) Programming Languages and Systems. LNCS, vol. 7211, pp. 397–416. Springer, Heidelberg (2012) · Zbl 1352.68131 · doi:10.1007/978-3-642-28869-2_20
[23] Firsov, D., Uustalu, T.: Certified CYK parsing of context-free languages. J. Log. Algebraic Methods Program. 83(56), 459–468 (2014). The 24th Nordic Workshop on Programming Theory (NWPT 2012) · Zbl 1371.68137 · doi:10.1016/j.jlamp.2014.09.002
[24] Barthwal, A., Norrish, M.: A formalisation of the normal forms of context-free grammars in HOL4. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 95–109. Springer, Heidelberg (2010) · Zbl 1287.68151 · doi:10.1007/978-3-642-15205-4_11
[25] Barthwal, A., Norrish, M.: Mechanisation of PDA and grammar equivalence for context-free languages. In: Dawar, A., de Queiroz, R. (eds.) WoLLIC 2010. LNCS, vol. 6188, pp. 125–135. Springer, Heidelberg (2010) · Zbl 1253.68201 · doi:10.1007/978-3-642-13824-9_11
[26] Barthwal, A., Norrish, M.: A mechanisation of some context-free language theory in HOL4. J. Comput. Syst. Sci. 80(2), 346–362 (2014). WoLLIC 2010 Special Issue, Dawar, A., de Queiroz, R. (eds.) · Zbl 1433.68531 · doi:10.1016/j.jcss.2013.05.003
[27] Barthwal, A.: A formalisation of the theory of context-free languages in higher order logic. Ph.D. thesis, The Australian National Universityd (2010). https://digitalcollections.anu.edu.au/bitstream/1885/16399/1/Barthwal%20Thesis%202010.pdf . Accessed 27 Nov 2015 · Zbl 1287.68151
[28] Firsov, D., Uustalu, T.: Certified normalization of context-free grammars. In: Proceedings of the 2015 Conference on Certified Programs and Proofs. CPP 2015, pp. 167–174. ACM, New York (2015) · doi:10.1145/2676724.2693177
[29] Doczkal, C., Kaiser, J.-O., Smolka, G.: A constructive theory of regular languages in Coq. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 82–97. Springer, Heidelberg (2013) · Zbl 1426.68143 · doi:10.1007/978-3-319-03545-1_6
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.