{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:03:29Z","timestamp":1767927809093,"version":"3.49.0"},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"1-4","license":[{"start":{"date-parts":[[2018,3,10]],"date-time":"2018-03-10T00:00:00Z","timestamp":1520640000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["678157"],"award-info":[{"award-number":["678157"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-11-IDEX-0007"],"award-info":[{"award-number":["ANR-11-IDEX-0007"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2018,6]]},"DOI":"10.1007\/s10817-018-9460-x","type":"journal-article","created":{"date-parts":[[2018,3,10]],"date-time":"2018-03-10T10:48:26Z","timestamp":1520678906000},"page":"521-553","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Regular Language Representations in the Constructive Type Theory of Coq"],"prefix":"10.1007","volume":"61","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4450-0184","authenticated-orcid":false,"given":"Christian","family":"Doczkal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gert","family":"Smolka","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,3,10]]},"reference":[{"issue":"4","key":"9460_CR1","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"1","author":"M Abadi","year":"1991","unstructured":"Abadi, M., Cardelli, L., Curien, P., L\u00e9vy, J.: Explicit substitutions. J. Funct. Program. 1(4), 375\u2013416 (1991)","journal-title":"J. Funct. Program."},{"key":"9460_CR2","doi-asserted-by":"crossref","unstructured":"Berghofer, S., Reiter, M.: Formalizing the logic-automaton connection. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics (TPHOLs 2009). LNCS, vol. 5674, pp. 147\u2013163. Springer (2009)","DOI":"10.1007\/978-3-642-03359-9_12"},{"key":"9460_CR3","doi-asserted-by":"crossref","unstructured":"Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.): Interactive Theorem Proving\u20144th International Conference, ITP 2013, Rennes, France, July 22\u201326, 2013. Proceedings, LNCS, vol. 7998. Springer (2013)","DOI":"10.1007\/978-3-642-39634-2"},{"issue":"1:16","key":"9460_CR4","first-page":"1","volume":"8","author":"T Braibant","year":"2012","unstructured":"Braibant, T., Pous, D.: Deciding kleene algebras in Coq. Log. Methods. Comput. Sci. 8(1:16), 1\u201342 (2012)","journal-title":"Log. Methods. Comput. Sci."},{"issue":"4","key":"9460_CR5","doi-asserted-by":"publisher","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"},{"key":"9460_CR6","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1002\/malq.19600060105","volume":"6","author":"JR B\u00fcchi","year":"1960","unstructured":"B\u00fcchi, J.R.: Weak second-order arithmetic and finite automata. Zeitschr. f. math. Logic und Grundladen d. Math. 6, 66\u201392 (1960)","journal-title":"Zeitschr. f. math. Logic und Grundladen d. Math."},{"key":"9460_CR7","doi-asserted-by":"crossref","unstructured":"Cohen, C.: Pragmatic quotient types in Coq. In: Blazy et\u00a0al. [3], pp. 213\u2013228","DOI":"10.1007\/978-3-642-39634-2_17"},{"key":"9460_CR8","doi-asserted-by":"crossref","first-page":"213","DOI":"10.7551\/mitpress\/5641.003.0014","volume-title":"Proof, Language, and Interaction","author":"RL Constable","year":"2000","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. The MIT Press, Cambridge (2000)"},{"key":"9460_CR9","doi-asserted-by":"crossref","unstructured":"Coquand, T., Siles, V.: A decision procedure for regular expression equivalence in type theory. In: Jouannaud, J.P., Shao, Z. (eds.) Certified Programs and Proofs (CPP 2011). LNCS, vol. 7086, pp. 119\u2013134. Springer (2011)","DOI":"10.1007\/978-3-642-25379-9_11"},{"key":"9460_CR10","unstructured":"Doczkal, C., Kaiser, J.O., Smolka, G.: Coq development accompanying this paper (Online Resource 1), https:\/\/github.com\/chdoc\/coq-reglang"},{"key":"9460_CR11","doi-asserted-by":"crossref","unstructured":"Doczkal, C., Kaiser, J., Smolka, G.: A constructive theory of regular languages in Coq. In: Gonthier, G., Norrish, M. (eds.) Certified Programs and Proofs (CPP 2013). LNCS, vol. 8307, pp. 82\u201397. Springer (2013)","DOI":"10.1007\/978-3-319-03545-1_6"},{"key":"9460_CR12","doi-asserted-by":"crossref","unstructured":"Doczkal, C., Smolka, G.: Two-way automata in Coq. In: Blanchette, J.C., Merz, S. (eds.) Interactive Theorem Proving (ITP 2016). LNCS, vol. 9807, pp. 151\u2013166. Springer (2016)","DOI":"10.1007\/978-3-319-43144-4_10"},{"key":"9460_CR13","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1090\/S0002-9947-1961-0139530-9","volume":"98","author":"CC Elgot","year":"1961","unstructured":"Elgot, C.C.: Decision problems of finite automata design and related arithmetics. Trans. Am. Math. Soc. 98, 21\u201351 (1961)","journal-title":"Trans. Am. Math. Soc."},{"key":"9460_CR14","unstructured":"Filli\u00e2tre, J.C.: Finite automata theory in Coq: A constructive proof of kleene\u2019s theorem. Tech. Rep. 97-04, LIP - ENS Lyon (1997)"},{"issue":"1","key":"9460_CR15","doi-asserted-by":"publisher","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. Logic 13(1), 4:1\u20134:19 (2012)","journal-title":"ACM Trans. Comput. Logic"},{"key":"9460_CR16","doi-asserted-by":"crossref","unstructured":"Gonthier, G., Mahboubi, A., Rideau, L., Tassi, E., Th\u00e9ry, L.: A modular formalisation of finite group theory. In: Schneider, K., Brandt, J. (eds.) Theorem Proving in Higher Order Logics (TPHOLs 2007). LNCS, vol. 4732, pp. 86\u2013101. Springer (2007)","DOI":"10.1007\/978-3-540-74591-4_8"},{"key":"9460_CR17","doi-asserted-by":"crossref","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.): Automata, logics, and infinite games: a guide to current research [outcome of a Dagstuhl seminar, February 2001], LNCS, vol. 2500. Springer (2002)","DOI":"10.1007\/3-540-36387-4"},{"issue":"4","key":"9460_CR18","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1017\/S0956796898003153","volume":"8","author":"M Hedberg","year":"1998","unstructured":"Hedberg, M.: A coherence theorem for Martin-L\u00f6f\u2019s type theory. J. Funct. Program. 8(4), 413\u2013436 (1998)","journal-title":"J. Funct. Program."},{"key":"9460_CR19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18090-3","volume-title":"Automatentheorie und Logik","author":"M Hofmann","year":"2011","unstructured":"Hofmann, M., Lange, M.: Automatentheorie und Logik. eXamen.press, Springer, Berlin (2011)"},{"key":"9460_CR20","volume-title":"Introduction to Automata Theory, Languages, and Computation - international edition (2. ed)","author":"JE Hopcroft","year":"2001","unstructured":"Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation - international edition (2. ed). Addison-Wesley, Boston (2001)"},{"key":"9460_CR21","doi-asserted-by":"crossref","unstructured":"Johnsonbaugh, R., Miller, D.P.: Converses of pumping lemmas. In: Austing, R.H., Cassel, L.N., Miller, J.E., Joyce, D.T. (eds.) Proceedings of the 21st SIGCSE Technical Symposium on Computer Science Education, 1990, Washington, DC, USA, 1990. pp. 27\u201330. ACM (1990)","DOI":"10.1145\/323410.319073"},{"key":"9460_CR22","volume-title":"Automata Theory and its Applications","author":"B Khoussainov","year":"2012","unstructured":"Khoussainov, B., Nerode, A.: Automata Theory and its Applications. Springer, Berlin (2012)"},{"key":"9460_CR23","first-page":"3","volume-title":"Automata Studies","author":"SC Kleene","year":"1956","unstructured":"Kleene, S.C.: Representation of events in nerve nets and finite automata. In: Shannon, C.E., McCarthy, J. (eds.) Automata Studies, pp. 3\u201342. Princeton University Press, Princeton (1956)"},{"key":"9460_CR24","volume-title":"Automata and computability. Undergraduate texts in computer science","author":"D Kozen","year":"1997","unstructured":"Kozen, D.: Automata and computability. Undergraduate texts in computer science. Springer, Berlin (1997)"},{"issue":"1","key":"9460_CR25","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. Reason. 49(1), 95\u2013106 (2012)","journal-title":"J. Autom. Reason."},{"issue":"3","key":"9460_CR26","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1016\/j.jlamp.2014.12.004","volume":"84","author":"N Moreira","year":"2015","unstructured":"Moreira, N., Pereira, D., de Sousa, S.M.: Deciding kleene algebra terms equivalence in Coq. J. Log. Algebr. Methods Program. 84(3), 377\u2013401 (2015)","journal-title":"J. Log. Algebr. Methods Program."},{"key":"9460_CR27","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Verified lexical analysis. In: Grundy, J., Newey, M.C. (eds.) Theorem Proving in Higher Order Logics (TPHOLs \u201998). LNCS, vol. 1479, pp. 1\u201315. Springer (1998)","DOI":"10.1007\/BFb0055126"},{"key":"9460_CR28","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: A formalisation of finite automata using hereditarily finite sets. In: Felty, A.P., Middeldorp, A. (eds.) Automated deduction (CADE-25). LNCS, vol. 9195, pp. 231\u2013245. Springer (2015)","DOI":"10.1007\/978-3-319-21401-6_15"},{"issue":"2\u20133","key":"9460_CR29","doi-asserted-by":"crossref","first-page":"225","DOI":"10.3233\/FI-2013-879","volume":"126","author":"G Pighizzini","year":"2013","unstructured":"Pighizzini, G.: Two-way finite automata: old and recent results. Fundam. Inform. 126(2\u20133), 225\u2013246 (2013)","journal-title":"Fundam. Inform."},{"key":"9460_CR30","doi-asserted-by":"crossref","unstructured":"Pous, D.: Kleene algebra with tests and coq tools for while programs. In: Blazy et\u00a0al. [3], pp. 180\u2013196","DOI":"10.1007\/978-3-642-39634-2_15"},{"issue":"2","key":"9460_CR31","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1147\/rd.32.0114","volume":"3","author":"MO Rabin","year":"1959","unstructured":"Rabin, M.O., Scott, D.: Finite automata and their decision problems. IBM J. Res. Dev. 3(2), 114\u2013125 (1959)","journal-title":"IBM J. Res. Dev."},{"key":"9460_CR32","doi-asserted-by":"crossref","unstructured":"Reinhardt, K.: The complexity of translating logic to finite automata. In: Gr\u00e4del et\u00a0al. [17], pp. 231\u2013238","DOI":"10.1007\/3-540-36387-4_13"},{"key":"9460_CR33","doi-asserted-by":"crossref","unstructured":"Rosenberg, A.L.: State. In: Goldreich, O., Rosenberg, A.L., Selman, A.L. (eds.) Theoretical computer science, essays in memory of Shimon even. LNCS, vol. 3895, pp. 375\u2013398. Springer (2006)","DOI":"10.1007\/11685654_16"},{"key":"9460_CR34","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1147\/rd.32.0198","volume":"3","author":"J Shepherdson","year":"1959","unstructured":"Shepherdson, J.: The reduction of two-way automata to one-way automata. IBM J. Res. Dev. 3, 198\u2013200 (1959)","journal-title":"IBM J. Res. Dev."},{"key":"9460_CR35","unstructured":"The Coq Proof Assistant: http:\/\/coq.inria.fr"},{"key":"9460_CR36","unstructured":"The Mathematical Components Project: http:\/\/math-comp.github.io\/math-comp\/"},{"key":"9460_CR37","first-page":"326","volume":"140","author":"BA Trakhtenbrot","year":"1961","unstructured":"Trakhtenbrot, B.A.: Finite automata and the logic of monadic predicates. Dokl. Akad. Nauk SSSR 140, 326\u2013329 (1961)","journal-title":"Dokl. Akad. Nauk SSSR"},{"key":"9460_CR38","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1017\/S0956796815000246","volume":"25","author":"D Traytel","year":"2015","unstructured":"Traytel, D., Nipkow, T.: Verified decision procedures for MSO on words based on derivatives of regular expressions. J. Funct. Program. 25, 1\u201330 (2015)","journal-title":"J. Funct. Program."},{"issue":"5","key":"9460_CR39","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1016\/0020-0190(89)90205-6","volume":"30","author":"MY Vardi","year":"1989","unstructured":"Vardi, M.Y.: A note on the reduction of two-way automata to one-way automata. Inf. Process. Lett. 30(5), 261\u2013264 (1989)","journal-title":"Inf. Process. Lett."},{"issue":"3","key":"9460_CR40","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1016\/0020-0190(90)90063-4","volume":"35","author":"MY Vardi","year":"1990","unstructured":"Vardi, M.Y.: Endmarkers can make a difference. Inf. Process. Lett. 35(3), 145\u2013148 (1990)","journal-title":"Inf. Process. Lett."},{"key":"9460_CR41","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: van Eekelen, M.C.J.D., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) Interactive Theorem Proving (ITP 2011). LNCS, vol. 6898, pp. 341\u2013356. Springer (2011)","DOI":"10.1007\/978-3-642-22863-6_25"},{"issue":"4","key":"9460_CR42","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. Reason. 52(4), 451\u2013480 (2014)","journal-title":"J. Autom. Reason."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-018-9460-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9460-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9460-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,1]],"date-time":"2024-07-01T22:52:20Z","timestamp":1719874340000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-018-9460-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,3,10]]},"references-count":42,"journal-issue":{"issue":"1-4","published-print":{"date-parts":[[2018,6]]}},"alternative-id":["9460"],"URL":"https:\/\/doi.org\/10.1007\/s10817-018-9460-x","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,3,10]]},"assertion":[{"value":"1 April 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 March 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 March 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}