{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T06:25:05Z","timestamp":1745994305536,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642228629"},{"type":"electronic","value":"9783642228636"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-22863-6_25","type":"book-chapter","created":{"date-parts":[[2011,8,8]],"date-time":"2011-08-08T09:47:55Z","timestamp":1312796875000},"page":"341-356","source":"Crossref","is-referenced-by-count":14,"title":["A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl)"],"prefix":"10.1007","author":[{"given":"Chunhan","family":"Wu","sequence":"first","affiliation":[]},{"given":"Xingyuan","family":"Zhang","sequence":"additional","affiliation":[]},{"given":"Christian","family":"Urban","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"25_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/3-540-45842-5_2","volume-title":"Types for Proofs and Programs","author":"S. Berghofer","year":"2002","unstructured":"Berghofer, S., Nipkow, T.: Executing higher order logic. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol.\u00a02277, pp. 24\u201340. Springer, Heidelberg (2002)"},{"key":"25_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-642-03359-9_12","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Berghofer","year":"2009","unstructured":"Berghofer, S., Reiter, M.: Formalizing the logic-automaton connection. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 147\u2013163. Springer, Heidelberg (2009)"},{"key":"25_CR3","first-page":"481","volume":"11","author":"J.A. Brzozowski","year":"1964","unstructured":"Brzozowski, J.A.: Derivatives of Regular Expressions. J.\u00a0ACM\u00a011, 481\u2013494 (1964)","journal-title":"J.\u00a0ACM"},{"key":"25_CR4","doi-asserted-by":"crossref","first-page":"213","DOI":"10.7551\/mitpress\/5641.003.0014","volume-title":"Proof, Language, and Interaction","author":"R.L. Constable","year":"2000","unstructured":"Constable, R.L., Jackson, P.B., Naumov, P., Uribe, J.C.: Constructively Formalizing Automata Theory. In: Proof, Language, and Interaction, pp. 213\u2013238. MIT Press, Cambridge (2000)"},{"key":"25_CR5","unstructured":"Filli\u00e2tre, J.-C.: Finite Automata Theory in Coq: A Constructive Proof of Kleene\u2019s Theorem. Research Report 97\u201304, LIP - ENS Lyon (1997)"},{"key":"25_CR6","volume-title":"Formal Languages and Their Relation to Automata","author":"J.E. Hopcroft","year":"1969","unstructured":"Hopcroft, J.E., Ullman, J.D.: Formal Languages and Their Relation to Automata. Addison-Wesley, Reading (1969)"},{"key":"25_CR7","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1844-9","volume-title":"Automata and Computability","author":"D. Kozen","year":"1997","unstructured":"Kozen, D.: Automata and Computability. Springer, Heidelberg (1997)"},{"key":"25_CR8","doi-asserted-by":"crossref","unstructured":"Kraus, A., Nipkow, T.: Proof Pearl: Regular Expression Equivalence and Relation Algebra. To appear in Journal of Automated Reasoning (2011)","DOI":"10.1007\/s10817-011-9223-4"},{"key":"25_CR9","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)"},{"issue":"2","key":"25_CR10","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1017\/S0956796808007090","volume":"19","author":"S. Owens","year":"2009","unstructured":"Owens, S., Reppy, J., Turon, A.: Regular-Expression Derivatives Re-Examined. Journal of Functional Programming\u00a019(2), 173\u2013190 (2009)","journal-title":"Journal of Functional Programming"},{"issue":"4","key":"25_CR11","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/s10990-008-9038-0","volume":"21","author":"S. Owens","year":"2008","unstructured":"Owens, S., Slind, K.: Adapting Functional Programs to Higher Order Logic. Higher-Order and Symbolic Computation\u00a021(4), 377\u2013409 (2008)","journal-title":"Higher-Order and Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22863-6_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,9]],"date-time":"2024-04-09T19:18:17Z","timestamp":1712690297000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22863-6_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642228629","9783642228636"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22863-6_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}