{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T04:27:41Z","timestamp":1775881661685,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642288685","type":"print"},{"value":"9783642288692","type":"electronic"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28869-2_20","type":"book-chapter","created":{"date-parts":[[2012,3,22]],"date-time":"2012-03-22T20:44:36Z","timestamp":1332449076000},"page":"397-416","source":"Crossref","is-referenced-by-count":50,"title":["Validating LR(1) Parsers"],"prefix":"10.1007","author":[{"given":"Jacques-Henri","family":"Jourdan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fran\u00e7ois","family":"Pottier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xavier","family":"Leroy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"20_CR1","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X. Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Communications of the ACM\u00a052, 107\u2013115 (2009)","journal-title":"Communications of the ACM"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-642-00590-9_12","volume-title":"Programming Languages and Systems","author":"A. Barthwal","year":"2009","unstructured":"Barthwal, A., Norrish, M.: Verified, Executable Parsing. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol.\u00a05502, pp. 160\u2013174. Springer, Heidelberg (2009)"},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"Barthwal, A.: A formalisation of the theory of context-free languages in higher order logic. PhD thesis, Australian National University (December 2010)","DOI":"10.1007\/978-3-642-15205-4_11"},{"issue":"7","key":"20_CR4","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/362619.362625","volume":"14","author":"F.L. DeRemer","year":"1971","unstructured":"DeRemer, F.L.: Simple LR(k) grammars. Communications of the ACM\u00a014(7), 453\u2013460 (1971)","journal-title":"Communications of the ACM"},{"key":"20_CR5","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/BF00571461","volume":"2","author":"T. Anderson","year":"1973","unstructured":"Anderson, T., Eve, J., Horning, J.J.: Efficient LR(1) parsers. Acta Informatica\u00a02, 12\u201339 (1973)","journal-title":"Acta Informatica"},{"key":"20_CR6","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/BF00290336","volume":"7","author":"D. Pager","year":"1977","unstructured":"Pager, D.: A practical general method for constructing LR(k) parsers. Acta Informatica\u00a07, 249\u2013268 (1977)","journal-title":"Acta Informatica"},{"key":"20_CR7","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1016\/S0019-9958(65)90426-2","volume":"8","author":"D.E. Knuth","year":"1965","unstructured":"Knuth, D.E.: On the translation of languages from left to right. Information & Control\u00a08, 607\u2013639 (1965)","journal-title":"Information & Control"},{"key":"20_CR8","unstructured":"Pottier, F., R\u00e9gis-Gianas, Y.: The Menhir parser generator, \n                  \n                    http:\/\/gallium.inria.fr\/~fpottier\/menhir\/"},{"key":"20_CR9","unstructured":"Jourdan, J.H., Pottier, F., Leroy, X.: Coq code for validating LR(1) parsers, \n                  \n                    http:\/\/www.eleves.ens.fr\/home\/jjourdan\/parserValidator.tgz"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1007\/978-3-540-24725-8_26","volume-title":"Programming Languages and Systems","author":"J.-C. Filli\u00e2tre","year":"2004","unstructured":"Filli\u00e2tre, J.-C., Letouzey, P.: Functors for Proofs and Programs. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol.\u00a02986, pp. 370\u2013384. Springer, Heidelberg (2004)"},{"key":"20_CR11","unstructured":"ISO\/IEC: Programming languages \u2014 C (2007) International standard ISO\/IEC 9899:TC3"},{"key":"20_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-642-00722-4_9","volume-title":"Compiler Construction","author":"Y. Padioleau","year":"2009","unstructured":"Padioleau, Y.: Parsing C\/C++ Code without Pre-processing. In: de Moor, O., Schwartzbach, M.I. (eds.) CC 2009. LNCS, vol.\u00a05501, pp. 109\u2013125. Springer, Heidelberg (2009)"},{"issue":"2","key":"20_CR13","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1016\/j.entcs.2005.11.044","volume":"148","author":"F. Pottier","year":"2006","unstructured":"Pottier, F., R\u00e9gis-Gianas, Y.: Towards efficient, typed LR parsers. Electronic Notes in Theoretical Computer Science\u00a0148(2), 155\u2013180 (2006)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"Ford, B.: Packrat parsing: simple, powerful, lazy, linear time. In: ACM International Conference on Functional Programming (ICFP), pp. 36\u201347 (October 2002)","DOI":"10.1145\/583852.581483"},{"key":"20_CR15","doi-asserted-by":"crossref","unstructured":"Ford, B.: Parsing expression grammars: a recognition-based syntactic foundation. In: ACM Symposium on Principles of Programming Languages (POPL), pp. 111\u2013122 (January 2004)","DOI":"10.1145\/982962.964011"},{"key":"20_CR16","doi-asserted-by":"crossref","unstructured":"Warth, A., Douglass, J.R., Millstein, T.D.: Packrat parsers can support left recursion. In: ACM Workshop on Evaluation and Semantics-Based Program Manipulation (PEPM), pp. 103\u2013110 (January 2008)","DOI":"10.1145\/1328408.1328424"},{"key":"20_CR17","doi-asserted-by":"crossref","unstructured":"Koprowski, A., Binsztok, H.: TRX: A formally verified parser interpreter. Logical Methods in Computer Science 7 (2011)","DOI":"10.2168\/LMCS-7(2:18)2011"},{"key":"20_CR18","unstructured":"Wisnesky, R., Malecha, G., Morrisett, G.: Certified web services in Ynot. In: Workshop on Automated Specification and Verification of Web Systems (July 2009)"},{"key":"20_CR19","unstructured":"Samet, H.: Automatically Proving the Correctness of Translations Involving Optimized Code. PhD thesis, Stanford University (1975)"},{"key":"20_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/BFb0054170","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Pnueli","year":"1998","unstructured":"Pnueli, A., Siegel, M., Singerman, E.: Translation Validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 151\u2013166. Springer, Heidelberg (1998)"},{"key":"20_CR21","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Translation validation for an optimizing compiler. In: ACM Conference on Programming Language Design and Implementation (PLDI), pp. 83\u201395. ACM Press (2000)","DOI":"10.1145\/358438.349314"},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"Tristan, J.B., Leroy, X.: A simple, verified validator for software pipelining. In: ACM Symposium on Principles of Programming Languages (POPL), pp. 83\u201392. ACM Press (2010)","DOI":"10.1145\/1707801.1706311"},{"key":"20_CR23","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1145\/1146809.1146811","volume":"28","author":"G. Klein","year":"2006","unstructured":"Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. ACM Transactions on Programming Languages and Systems\u00a028, 619\u2013695 (2006)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"20_CR24","unstructured":"Aho, A.V., Ullman, J.D.: The theory of parsing, translation, and compiling. Prentice-Hall (1972)"},{"key":"20_CR25","doi-asserted-by":"crossref","unstructured":"Sozeau, M.: Program-ing finger trees in Coq. In: ACM International Conference on Functional Programming (ICFP), pp. 13\u201324 (September 2007)","DOI":"10.1145\/1291151.1291156"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28869-2_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T00:46:33Z","timestamp":1558313193000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28869-2_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642288685","9783642288692"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28869-2_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}