{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T05:44:02Z","timestamp":1748583842767,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":5,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642005893"},{"type":"electronic","value":"9783642005909"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-00590-9_12","type":"book-chapter","created":{"date-parts":[[2009,3,27]],"date-time":"2009-03-27T08:05:58Z","timestamp":1238141158000},"page":"160-174","source":"Crossref","is-referenced-by-count":26,"title":["Verified, Executable Parsing"],"prefix":"10.1007","author":[{"given":"Aditi","family":"Barthwal","sequence":"first","affiliation":[]},{"given":"Michael","family":"Norrish","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/11813040_31","volume-title":"FM 2006: Formal Methods","author":"S. Blazy","year":"2006","unstructured":"Blazy, S., Dargaye, Z., Leroy, X.: Formal verification of a C compiler front-end. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 460\u2013475. Springer, Heidelberg (2006)"},{"volume-title":"Introduction to HOL: a theorem proving environment for higher order logic","year":"1993","unstructured":"Gordon, M.J.C., Melham, T. (eds.): Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, Cambridge (1993)","key":"12_CR2"},{"key":"12_CR3","volume-title":"Introduction to Automata Theory, Languages and Computation","author":"J.E. Hopcroft","year":"1979","unstructured":"Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and Computation. Addison-Wesley, Reading (1979)"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0055126","volume-title":"Theorem Proving in Higher Order Logics","author":"T. Nipkow","year":"1998","unstructured":"Nipkow, T.: Verified lexical analysis. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol.\u00a01479, pp. 1\u201315. Springer, Heidelberg (1998)"},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-540-71067-7_6","volume-title":"Theorem Proving in Higher Order Logics","author":"K. Slind","year":"2008","unstructured":"Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 28\u201332. Springer, Heidelberg (2008), \n                    \n                      http:\/\/hol.sourceforge.net"}],"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-00590-9_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,7]],"date-time":"2019-03-07T02:23:50Z","timestamp":1551925430000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-00590-9_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642005893","9783642005909"],"references-count":5,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-00590-9_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}