{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:42:00Z","timestamp":1742913720480,"version":"3.40.3"},"publisher-location":"Cham","reference-count":15,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319214009"},{"type":"electronic","value":"9783319214016"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21401-6_15","type":"book-chapter","created":{"date-parts":[[2015,7,24]],"date-time":"2015-07-24T10:13:46Z","timestamp":1437732826000},"page":"231-245","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["A Formalisation of Finite Automata Using Hereditarily Finite Sets"],"prefix":"10.1007","author":[{"given":"Lawrence C.","family":"Paulson","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,25]]},"reference":[{"issue":"2","key":"15_CR1","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10817-013-9284-7","volume":"52","author":"C Ballarin","year":"2014","unstructured":"Ballarin, C.: Locales: A module system for mathematical theories. J. Autom. Reasoning 52(2), 123\u2013153 (2014)","journal-title":"J. Autom. Reasoning"},{"issue":"1","key":"15_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-8(1:16)2012","volume":"8","author":"T Braibant","year":"2012","unstructured":"Braibant, T., Pous, D.: Deciding Kleene algebras in Coq. Log. Methods Comput. Sci. 8(1), 1\u201342 (2012)","journal-title":"Log. Methods Comput. Sci."},{"key":"15_CR3","unstructured":"Champarnaud, J., Khorsi, A., Parantho\u00ebn, T.: Split and join for minimizing: Brzozowski\u2019s algorithm. In: Bal\u00edk, M., Sim\u00e1nek, M. (eds.) The Prague Stringology Conference, pp. 96\u2013104. Czech Technical University, Department of Computer Science and Engineering (2002)"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Constable, R.L., Jackson, P.B., Naumov, P., Uribe, J.C.: Constructively formalizing automata theory. In: Plotkin, G.D., Stirling, C., Tofte, M. (eds.) Proof, Language, and Interaction, pp. 213\u2013238. MIT Press (2000)","DOI":"10.7551\/mitpress\/5641.003.0014"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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)"},{"key":"15_CR6","unstructured":"Hopcroft, J.E., Ullman, J.D.: Formal Languages and Their Relation to Automata. Addison-Wesley, Boston (1969)"},{"key":"15_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, New York (1997)"},{"issue":"1","key":"15_CR8","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/s10817-011-9223-4","volume":"49","author":"A Krauss","year":"2012","unstructured":"Krauss, A., Nipkow, T.: Proof pearl: regular expression equivalence and relation algebra. J. Autom. Reasoning 49(1), 95\u2013106 (2012)","journal-title":"J. Autom. Reasoning"},{"key":"15_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. 1479, pp. 1\u201315. Springer, Heidelberg (1998)"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"450","DOI":"10.1007\/978-3-319-08970-6_29","volume-title":"Interactive Theorem Proving","author":"T Nipkow","year":"2014","unstructured":"Nipkow, T., Traytel, D.: Unified decision procedures for regular expression equivalence. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 450\u2013466. Springer, Heidelberg (2014)"},{"issue":"4","key":"15_CR11","doi-asserted-by":"publisher","first-page":"658","DOI":"10.1145\/1183278.1183280","volume":"7","author":"LC Paulson","year":"2006","unstructured":"Paulson, L.C.: Defining functions on equivalence classes. ACM Trans. Comput. Logic 7(4), 658\u2013675 (2006)","journal-title":"ACM Trans. Comput. Logic"},{"key":"15_CR12","unstructured":"Paulson, L.C.: Finite automata in hereditarily finite set theory. Archive of Formal Proofs, February 2015. http:\/\/afp.sf.net\/entries\/Finite_Automata_HF.shtml, Formal proof development"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: A mechanised proof of G\u00f6del\u2019s incompleteness theorems using Nominal Isabelle. J. Autom. Reasoning 55(1), 1\u201337 (2015). Available online at http:\/\/link.springer.com\/article\/10.1007%2Fs10817-015-9322-8","DOI":"10.1007\/s10817-015-9322-8"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"\u015awierczkowski, S.: Finite sets and G\u00f6del\u2019s incompleteness theorems. Dissertationes Mathematicae 422, 1\u201358 (2003). http:\/\/journals.impan.gov.pl\/dm\/Inf\/422-0-1.html","DOI":"10.4064\/dm422-0-1"},{"issue":"4","key":"15_CR15","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/s10817-013-9297-2","volume":"52","author":"C Wu","year":"2014","unstructured":"Wu, C., Zhang, X., Urban, C.: A formalisation of the Myhill-Nerode theorem based on regular expressions. J. Autom. Reasoning 52(4), 451\u2013480 (2014)","journal-title":"J. Autom. Reasoning"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-25"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21401-6_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,10]],"date-time":"2024-06-10T05:00:33Z","timestamp":1717995633000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-21401-6_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319214009","9783319214016"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21401-6_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"25 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}