{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:21:28Z","timestamp":1740097288482,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662529201"},{"type":"electronic","value":"9783662529218"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-662-52921-8_21","type":"book-chapter","created":{"date-parts":[[2016,8,5]],"date-time":"2016-08-05T15:22:30Z","timestamp":1470410550000},"page":"338-357","source":"Crossref","is-referenced-by-count":2,"title":["On the Formalization of Some Results of Context-Free Language Theory"],"prefix":"10.1007","author":[{"given":"Marcus Vin\u00edcius Midena","family":"Ramos","sequence":"first","affiliation":[]},{"given":"Ruy J. G. B.","family":"de Queiroz","sequence":"additional","affiliation":[]},{"given":"Nelma","family":"Moreira","sequence":"additional","affiliation":[]},{"given":"Jos\u00e9 Carlos Bacelar","family":"Almeida","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,8,6]]},"reference":[{"key":"21_CR1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Springer, Heidelberg (2004)"},{"key":"21_CR2","volume-title":"Languages and Machines","author":"TA Sudkamp","year":"2006","unstructured":"Sudkamp, T.A.: Languages and Machines, 3rd edn. Addison-Wesley, Redwood City (2006)","edition":"3"},{"key":"21_CR3","volume-title":"Linguagens Formais: Teoria Modelagem e Implementa\u00e7\u00e3o","author":"MVM Ramos","year":"2009","unstructured":"Ramos, M.V.M., Neto, J.J., Vega, I.S.: Linguagens Formais: Teoria Modelagem e Implementa\u00e7\u00e3o. Bookman, Brisbane (2009)"},{"key":"21_CR4","unstructured":"Ramos, M.V.M.: Formalization of Context-Free Language Theory. Ph.D. thesis, Centro de Inform\u00e1tica-UFPE (2016). www.univasf.edu.br\/~marcus.ramos\/tese.pdf . Accessed 5 May 2016"},{"key":"21_CR5","unstructured":"Ramos, M.V.M.: Source files of [4] (2016). https:\/\/github.com\/mvmramos\/v1 . Accessed 3 May 2016"},{"key":"21_CR6","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1016\/S0019-9958(59)90362-6","volume":"2","author":"AN Chomsky","year":"1959","unstructured":"Chomsky, A.N.: On certain formal properties of grammar. Inf. Control 2, 137\u2013167 (1959)","journal-title":"Inf. Control"},{"key":"21_CR7","series-title":"Addison-Wesley Series in Logic","volume-title":"Language and Information: Selected Essays on Their Theory and Application","author":"Y Bar-Hillel","year":"1964","unstructured":"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)"},{"key":"21_CR8","volume-title":"Formal Languages and Their Relation to Automata","author":"JE Hopcroft","year":"1969","unstructured":"Hopcroft, J.E., Ullman, J.D.: Formal Languages and Their Relation to Automata. Addison-Wesley Longman Publishing Co., Inc., Boston (1969)"},{"key":"21_CR9","volume-title":"Computability, Complexity, and Languages: Fundamentals of Theoretical Computer Science","author":"MD Davis","year":"1994","unstructured":"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)","edition":"2"},{"key":"21_CR10","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-1844-9","volume-title":"Automata and Computability","author":"DC Kozen","year":"1997","unstructured":"Kozen, D.C.: Automata and Computability. Springer, Heidelberg (1997)"},{"key":"21_CR11","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1145\/568438.568455"},{"key":"21_CR12","volume-title":"The Mathematical Theory of Context-Free Languages","author":"S Ginsburg","year":"1966","unstructured":"Ginsburg, S.: The Mathematical Theory of Context-Free Languages. McGraw-Hill Inc., New York (1966)"},{"key":"21_CR13","volume-title":"Machines, Languages and Computation","author":"PJ Denning","year":"1978","unstructured":"Denning, P.J., Dennis, J.B., Qualitz, J.E.: Machines, Languages and Computation. Prentice-Hall, Upper Saddle River (1978)"},{"key":"21_CR14","volume-title":"Theory of Computation: Formal Languages, Automata, and Complexity","author":"JG Brookshear","year":"1989","unstructured":"Brookshear, J.G.: Theory of Computation: Formal Languages, Automata, and Complexity. Benjamin-Cummings Publishing Co., Inc., Redwood City (1989)"},{"key":"21_CR15","volume-title":"Elements of the Theory of Computation","author":"HR Lewis","year":"1998","unstructured":"Lewis, H.R., Papadimitriou, C.H.: Elements of the Theory of Computation, 2nd edn. Prentice Hall PTR, Upper Saddle River (1998)","edition":"2"},{"key":"21_CR16","volume-title":"Introduction to the Theory of Computation","author":"M Sipser","year":"2005","unstructured":"Sipser, M.: Introduction to the Theory of Computation, 2nd edn. International Thomson Publishing, Toronto (2005)","edition":"2"},{"key":"21_CR17","volume-title":"Introduction to Formal Language Theory","author":"MA Harrison","year":"1978","unstructured":"Harrison, M.A.: Introduction to Formal Language Theory, 1st edn. Addison-Wesley Longman Publishing Co., Inc., Boston (1978)","edition":"1"},{"key":"21_CR18","unstructured":"Amarilli, A., Jeanmougin, M.: A proof of the pumping lemma for context-free languages through pushdown automata. CoRR abs\/1207.2819 (2012)"},{"key":"21_CR19","unstructured":"INRIA: Coq users\u2019 contributions (2015). http:\/\/www.lix.polytechnique.fr\/coq\/pylons\/contribs\/index . Accessed 26 Oct 2015"},{"key":"21_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1007\/978-3-642-11957-6_19","volume-title":"Programming Languages and Systems","author":"A Koprowski","year":"2010","unstructured":"Koprowski, A., Binsztok, H.: TRX: a formally verified parser interpreter. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 345\u2013365. Springer, Heidelberg (2010). http:\/\/dx.doi.org\/10.1007\/978-3-642-11957-6_19 . Accessed 26 Oct 2015"},{"key":"21_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/978-3-642-25379-9_10","volume-title":"Certified Programs and Proofs","author":"T Ridge","year":"2011","unstructured":"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\u2013118. Springer, Heidelberg (2011)"},{"key":"21_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1007\/978-3-642-28869-2_20","volume-title":"Programming Languages and Systems","author":"J-H Jourdan","year":"2012","unstructured":"Jourdan, J.-H., Pottier, F., Leroy, X.: Validating LR(1) parsers. In: Seidl, H. (ed.) Programming Languages and Systems. LNCS, vol. 7211, pp. 397\u2013416. Springer, Heidelberg (2012)"},{"issue":"56","key":"21_CR23","doi-asserted-by":"crossref","first-page":"459","DOI":"10.1016\/j.jlamp.2014.09.002","volume":"83","author":"D Firsov","year":"2014","unstructured":"Firsov, D., Uustalu, T.: Certified CYK parsing of context-free languages. J. Log. Algebraic Methods Program. 83(56), 459\u2013468 (2014). The 24th Nordic Workshop on Programming Theory (NWPT 2012)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"21_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1007\/978-3-642-15205-4_11","volume-title":"Computer Science Logic","author":"A Barthwal","year":"2010","unstructured":"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\u2013109. Springer, Heidelberg (2010)"},{"key":"21_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/978-3-642-13824-9_11","volume-title":"Logic, Language, Information and Computation","author":"A Barthwal","year":"2010","unstructured":"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\u2013135. Springer, Heidelberg (2010)"},{"issue":"2","key":"21_CR26","doi-asserted-by":"crossref","first-page":"346","DOI":"10.1016\/j.jcss.2013.05.003","volume":"80","author":"A Barthwal","year":"2014","unstructured":"Barthwal, A., Norrish, M.: A mechanisation of some context-free language theory in HOL4. J. Comput. Syst. Sci. 80(2), 346\u2013362 (2014). WoLLIC 2010 Special Issue, Dawar, A., de Queiroz, R. (eds.)","journal-title":"J. Comput. Syst. Sci."},{"key":"21_CR27","unstructured":"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"},{"key":"21_CR28","doi-asserted-by":"crossref","unstructured":"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\u2013174. ACM, New York (2015)","DOI":"10.1145\/2676724.2693177"},{"key":"21_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1007\/978-3-319-03545-1_6","volume-title":"Certified Programs and Proofs","author":"C Doczkal","year":"2013","unstructured":"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\u201397. Springer, Heidelberg (2013)"}],"container-title":["Lecture Notes in Computer Science","Logic, Language, Information, and Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-52921-8_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,5]],"date-time":"2022-07-05T06:11:43Z","timestamp":1657001503000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-52921-8_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662529201","9783662529218"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-52921-8_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}