{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,5,23]],"date-time":"2024-05-23T15:40:10Z","timestamp":1716478810681},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2014,1,25]],"date-time":"2014-01-25T00:00:00Z","timestamp":1390608000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2014,4]]},"DOI":"10.1007\/s10817-013-9297-2","type":"journal-article","created":{"date-parts":[[2014,1,24]],"date-time":"2014-01-24T07:48:51Z","timestamp":1390549731000},"page":"451-480","source":"Crossref","is-referenced-by-count":7,"title":["A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions"],"prefix":"10.1007","volume":"52","author":[{"given":"Chunhan","family":"Wu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xingyuan","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christian","family":"Urban","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,1,25]]},"reference":[{"key":"9297_CR1","doi-asserted-by":"crossref","unstructured":"Almeida, J.B., Moriera, N., Pereira, D., de Sousa, S.M.: Partial derivative automata formalized in Coq. In: Proceedings of the 15th International Conference on Implementation and Application of Automata, vol. 6482, pp. 59\u201368. LNCS (2010)","DOI":"10.1007\/978-3-642-18098-9_7"},{"key":"9297_CR2","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/0304-3975(95)00182-4","volume":"155","author":"V Antimirov","year":"1995","unstructured":"Antimirov, V.: Partial derivatives of regular expressions and finite automata constructions. Theor. Comput. Sci. 155, 291\u2013319 (1995)","journal-title":"Theor. Comput. Sci"},{"key":"9297_CR3","doi-asserted-by":"crossref","unstructured":"Asperti, A.: A compact proof of decidability for regular expression equivalence. In: Proceedings of the 3rd International Conference on Interactive Theorem Proving, vol. 7406, pp. 283\u2013298. LNCS (2012)","DOI":"10.1007\/978-3-642-32347-8_19"},{"key":"9297_CR4","doi-asserted-by":"crossref","unstructured":"Berghofer, S., Nipkow, T.: Executing higher order logic. In: Proceedings of the International Workshop on Types for Proofs and Programs, vol. 2277, pp. 24\u201340. LNCS (2002)","DOI":"10.1007\/3-540-45842-5_2"},{"key":"9297_CR5","doi-asserted-by":"crossref","unstructured":"Berghofer, S., Reiter, M.: Formalizing the logic-automaton connection. In: Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, vol. 5674, pp. 147\u2013163. LNCS (2009)","DOI":"10.1007\/978-3-642-03359-9_12"},{"key":"9297_CR6","unstructured":"Braibant, T.: Kleene Algebras, Rewriting Modulo AC, and and Circuits in Coq. Ph.D. thesis, University of Grenoble (2012)"},{"issue":"4","key":"9297_CR7","doi-asserted-by":"crossref","first-page":"481","DOI":"10.1145\/321239.321249","volume":"11","author":"JA Brzozowski","year":"1964","unstructured":"Brzozowski, J.A.: Derivatives of regular expressions. J. ACM 11(4), 481\u2013494 (1964)","journal-title":"J. ACM"},{"issue":"2","key":"9297_CR8","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5(2), 56\u201368 (1940)","journal-title":"J. Symb. Log."},{"key":"9297_CR9","doi-asserted-by":"crossref","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 (2000)","DOI":"10.7551\/mitpress\/5641.003.0014"},{"key":"9297_CR10","doi-asserted-by":"crossref","unstructured":"Coquand, T., Siles, V.: A decision procedure for regular expression equivalence in type theory. In: Proceedings of the 1st Conference on Certified Programs and Proofs, vol. 7086, pp. 119\u2013134. LNCS (2011)","DOI":"10.1007\/978-3-642-25379-9_11"},{"key":"9297_CR11","doi-asserted-by":"crossref","unstructured":"Doczkal, C., Kaiser, J.O., Smolka, G.: A Constructive Theory of Regular Languages in Coq. Accepted for publication. In: Proceedings of the 3rd International Conference on Certified Programs and Proofs. (2013)","DOI":"10.1007\/978-3-319-03545-1_6"},{"issue":"3","key":"9297_CR12","doi-asserted-by":"crossref","first-page":"577","DOI":"10.1007\/s00224-008-9111-4","volume":"45","author":"SA Fenner","year":"2009","unstructured":"Fenner, S.A., Gasarch, W.I., Postow, B.: The complexity of finding SUBSEQ(A). Theor. Comput. Syst. 45(3), 577\u2013612 (2009)","journal-title":"Theor. Comput. Syst"},{"key":"9297_CR13","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":"9297_CR14","unstructured":"Fortnow, L., Gasarch, W.I.: Proving DFA-Langs Closed Under Concat and * Without Using Equiv to NDFA\u2019s. Retrieved today, from http:\/\/blog.computationalcomplexity.org (2013)"},{"issue":"1","key":"9297_CR15","doi-asserted-by":"crossref","first-page":"4:1","DOI":"10.1145\/2071368.2071372","volume":"13","author":"W Gelade","year":"2012","unstructured":"Gelade, W., Neven, F.: Succinctness of the complement and intersection of regular expressions. ACM Trans. Comput. Log. 13(1), 4:1\u20134:21 (2012)","journal-title":"ACM Trans. Comput. Log"},{"key":"9297_CR16","unstructured":"Haftmann, F.: Code Generation from Specifications in Higher-Order Logic. Ph.D. thesis, Technical University of Munich (2009)"},{"key":"9297_CR17","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1016\/S0021-9800(69)80111-0","volume":"6","author":"LH Haines","year":"1969","unstructured":"Haines, L.H.: On free monoids partially ordered by embedding. J. Comb. Theor. 6, 94\u201398 (1969)","journal-title":"J. Comb. Theor"},{"issue":"4","key":"9297_CR18","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1017\/S0956796899003378","volume":"9","author":"R Harper","year":"1999","unstructured":"Harper, R.: Proof-directed debugging. J. Funct. Program. 9(4), 463\u2013469 (1999)","journal-title":"J. Funct. Program."},{"key":"9297_CR19","unstructured":"Hopcroft, J.E., Ullman, J.D.: Formal Languages and Their Relation to Automata. Addison-Wesley, Reading (1969)"},{"key":"9297_CR20","doi-asserted-by":"crossref","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":"9297_CR21","doi-asserted-by":"crossref","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. Reason. 49(1), 95\u2013106 (2012)","journal-title":"J. Autom. Reason"},{"key":"9297_CR22","doi-asserted-by":"crossref","unstructured":"Lammich, P., Tuerk, T.: Applying data refinement for monadic programs to Hopcroft\u2019s Algorithm. In: Proceedings of the 3rd International Conference on Interactive Theorem Proving, vol. 7406, pp. 166\u2013182. LNCS (2012)","DOI":"10.1007\/978-3-642-32347-8_12"},{"key":"9297_CR23","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Verified lexical analysis. In: Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics, vol. 1479, pp. 1\u201315. LNCS (1998)","DOI":"10.1007\/BFb0055126"},{"key":"9297_CR24","unstructured":"Nipkow, T.: Gauss-Jordan elimination for matrices represented as functions. In: Klein, G., Nipkow, T., Paulson, L. (eds.) The Archive of Formal Proofs, http:\/\/afp.sourceforge.net\/entries\/Gauss-Jordan-Elim-Fun.shtml . Formal proof development, 2011"},{"issue":"2","key":"9297_CR25","doi-asserted-by":"crossref","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. J. Funct. Program. 19(2), 173\u2013190 (2009)","journal-title":"J. Funct. Program."},{"issue":"4","key":"9297_CR26","doi-asserted-by":"crossref","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 Symb. Comput. 21(4), 377\u2013409 (2008)","journal-title":"Higher-Order Symb. Comput"},{"key":"9297_CR27","unstructured":"Rosenberg, A.L.: A Big Ideas Approach to the Theory of Computation. Course notes for CMPSCI 401 at the University of Massachusetts (2006)"},{"key":"9297_CR28","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139195218","volume-title":"Elements of Automata Theory","author":"J Sakarovitch","year":"2009","unstructured":"Sakarovitch, J.: Elements of Automata Theory. Cambridge University Press, Cambridge (2009)"},{"key":"9297_CR29","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511808876","volume-title":"A Second Course in Formal Languages and Automata Theory","author":"J Shallit","year":"2008","unstructured":"Shallit, J.: A Second Course in Formal Languages and Automata Theory. Cambridge University Press, Cambridge (2008)"},{"key":"9297_CR30","doi-asserted-by":"crossref","unstructured":"Sternagel, C.: Certified kruskals tree theorem. Accepted for publication In: Proceedings of the 3rd International Conference on Certified Programs and Proofs. (2013)","DOI":"10.1007\/978-3-319-03545-1_12"},{"key":"9297_CR31","doi-asserted-by":"crossref","unstructured":"Sulzmann, M., Lu, K.Z.M.: Regular expression sub-matching using partial derivatives. In: Proceedings of the 14th Symposium on Principles and Practice of Declarative Programming (PPDP), pp. 79\u201390. ACM (2012)","DOI":"10.1145\/2370776.2370788"},{"key":"9297_CR32","doi-asserted-by":"crossref","unstructured":"Wu, C., Zhang, X., Urban, C.: A formalisation of the Myhill-Nerode theorem based on regular expressions (Proof Pearl). In: Proceedings of the 2nd International Conference on Interactive Theorem Proving, vol. 6898, pp. 341\u2013356. LNCS (2011)","DOI":"10.1007\/978-3-642-22863-6_25"},{"key":"9297_CR33","unstructured":"Wu, C., Zhang, X., Urban, C.: The Myhill-Nerode theorem based on regular expressions. In: Klein, G., Nipkow, T., Paulson, L. (eds) The Archive of Formal Proofs, http:\/\/afp.sourceforge.net\/entries\/Myhill-Nerode.shtml . Formal proof development, 2011"},{"issue":"6","key":"9297_CR34","doi-asserted-by":"crossref","first-page":"663","DOI":"10.1017\/S0956796806006149","volume":"16","author":"K Yi","year":"2006","unstructured":"Yi, K.: Educational pearl: Proof-Directed Debugging revisited for a first-order version. J. Funct. Program. 16(6), 663\u2013670 (2006)","journal-title":"J. Funct. Program"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9297-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-013-9297-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9297-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,23]],"date-time":"2024-05-23T15:19:31Z","timestamp":1716477571000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-013-9297-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,1,25]]},"references-count":34,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2014,4]]}},"alternative-id":["9297"],"URL":"https:\/\/doi.org\/10.1007\/s10817-013-9297-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,1,25]]}}}