{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:20:56Z","timestamp":1747592456079},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642119569"},{"type":"electronic","value":"9783642119576"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-11957-6_19","type":"book-chapter","created":{"date-parts":[[2010,3,8]],"date-time":"2010-03-08T00:55:38Z","timestamp":1268009738000},"page":"345-365","source":"Crossref","is-referenced-by-count":17,"title":["TRX: A Formally Verified Parser Interpreter"],"prefix":"10.1007","author":[{"given":"Adam","family":"Koprowski","sequence":"first","affiliation":[]},{"given":"Henri","family":"Binsztok","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","volume-title":"Compilers: Principles, Techniques, and Tools","author":"A.V. Aho","year":"1986","unstructured":"Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison-Wesley, Reading (1986)"},{"key":"19_CR2","series-title":"Parsing","volume-title":"The Theory of Parsing, Translation and Compiling","author":"A.V. Aho","year":"1972","unstructured":"Aho, A.V., Ullman, J.D.: The Theory of Parsing, Translation and Compiling. Parsing, vol.\u00a0I. Prentice-Hall, Englewood Cliffs (1972)"},{"key":"19_CR3","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":"19_CR4","series-title":"Texts in Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, Heidelberg (2004)"},{"key":"19_CR5","volume-title":"Recursive Programming Techniques","author":"W.H. Burge","year":"1975","unstructured":"Burge, W.H.: Recursive Programming Techniques. Addison-Wesley, Reading (1975)"},{"key":"19_CR6","unstructured":"Cannasse, N.: Xml-light (2003), http:\/\/tech.motion-twin.com\/xmllight.html"},{"key":"19_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/10930755_18","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Chrzaszcz","year":"2003","unstructured":"Chrzaszcz, J.: Implementing modules in the Coq system. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 270\u2013286. Springer, Heidelberg (2003)"},{"issue":"1","key":"19_CR8","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/j.entcs.2005.11.024","volume":"151","author":"L. Cruz-Filipe","year":"2006","unstructured":"Cruz-Filipe, L., Letouzey, P.: A large-scale experiment in executing extracted programs. Electronic Notes in Theoretical Computer Science\u00a0151(1), 75\u201391 (2006)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"19_CR9","unstructured":"Danielsson, N.A., Norell, U.: Structurally recursive descent parsing (2008), Draft, http:\/\/www.cs.nott.ac.uk\/~nad\/publications"},{"key":"19_CR10","unstructured":"Durak, B.: Aurochs (2009), http:\/\/aurochs.fr\/"},{"key":"19_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"19_CR12","doi-asserted-by":"crossref","unstructured":"Ford, B.: Packrat parsing: a practical linear-time algorithm with backtracking. Master\u2019s thesis, Massachusetts Institute of Technology (2002)","DOI":"10.1145\/581478.581483"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"Ford, B.: Packrat parsing: simple, powerful, lazy, linear time, functional pearl. In: ICFP 2002, pp. 36\u201347 (2002)","DOI":"10.1145\/581478.581483"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"Ford, B.: Parsing expression grammars: a recognition-based syntactic foundation. In: POPL 2004, pp. 111\u2013122 (2004)","DOI":"10.1145\/964001.964011"},{"key":"19_CR15","volume-title":"The Java language specification","author":"J. Gosling","year":"2005","unstructured":"Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java language specification, 3rd edn. Addison-Wesley, Reading (2005)","edition":"3"},{"issue":"3","key":"19_CR16","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1017\/S0956796800000411","volume":"2","author":"G. Hutton","year":"1992","unstructured":"Hutton, G.: Higher-order functions for parsing. The Journal of Functional Programming\u00a02(3), 323\u2013343 (1992)","journal-title":"The Journal of Functional Programming"},{"issue":"7","key":"19_CR17","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(7), 107\u2013115 (2009)","journal-title":"Communications of the ACM"},{"key":"19_CR18","unstructured":"Leroy, X., et al.: Objective caml (1996), http:\/\/caml.inria.fr"},{"key":"19_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-540-69407-6_39","volume-title":"Logic and Theory of Algorithms","author":"P. Letouzey","year":"2008","unstructured":"Letouzey, P.: Extraction in Coq: An overview. In: Beckmann, A., Dimitracopoulos, C., L\u00f6we, B. (eds.) CiE 2008. LNCS, vol.\u00a05028, pp. 359\u2013369. Springer, Heidelberg (2008)"},{"key":"19_CR20","volume-title":"Lex & yacc","author":"J.R. Levine","year":"1992","unstructured":"Levine, J.R., Mason, T., Brown, D.: Lex & yacc. O\u2019Reilly, Sebastopol (1992)"},{"key":"19_CR21","unstructured":"McBride, C., McKinna, J.: Seeing and doing. Presentation at the Workshop on Termination and Type Theory (2002)"},{"key":"19_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/3-540-57877-3_18","volume-title":"Compiler Construction","author":"T.J. Parr","year":"1994","unstructured":"Parr, T.J., Quong, R.W.: Adding semantic and syntactic predicates to LL(k): pred-LL(k). In: Fritzson, P.A. (ed.) CC 1994. LNCS, vol.\u00a0786, pp. 263\u2013277. Springer, Heidelberg (1994)"},{"key":"19_CR23","unstructured":"Peyton-Jones, S., et al.: Haskell 98 language and libraries: The revised report (2002), http:\/\/haskell.org\/"},{"issue":"3-4","key":"19_CR24","first-page":"513","volume":"79","author":"R.R. Redziejowski","year":"2007","unstructured":"Redziejowski, R.R.: Parsing expression grammar as a primitive recursive-descent parser with backtracking. Fundamenta Informaticae\u00a079(3-4), 513\u2013524 (2007)","journal-title":"Fundamenta Informaticae"},{"key":"19_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-540-71067-7_23","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Sozeau","year":"2008","unstructured":"Sozeau, M., Oury, N.: First-class type classes. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 278\u2013293. Springer, Heidelberg (2008)"},{"issue":"4","key":"19_CR26","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1023\/A:1010035624696","volume":"11","author":"G.J. Sussman","year":"1998","unstructured":"Sussman, G.J., Steele Jr., G.L.: Scheme: A interpreter for extended lambda calculus. Higher-Order and Symbolic Computation\u00a011(4), 405\u2013439 (1998)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"19_CR27","unstructured":"The Agda team. The Agda wiki (2008), http:\/\/wiki.portal.chalmers.se\/agda\/"},{"key":"19_CR28","unstructured":"The Coq Development Team. The Coq proof assistant: Reference manual, version 8.2, 1989\u20132009, http:\/\/coq.inria.fr"},{"key":"19_CR29","doi-asserted-by":"crossref","unstructured":"Warth, A., Douglass, J.R., Millstein, T.D.: Packrat parsers can support left recursion. In: PEPM 2008, pp. 103\u2013110 (2008)","DOI":"10.1145\/1328408.1328424"},{"key":"19_CR30","unstructured":"Wisnesky, R., Malecha, G., Morrisett, G.: Certified web services in Ynot. In: Proceedings of WWV 2009, pp. 5\u201319 (2009)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-11957-6_19.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:45:43Z","timestamp":1606185943000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11957-6_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642119569","9783642119576"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11957-6_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}