{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:28:35Z","timestamp":1767929315677,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642140518","type":"print"},{"value":"9783642140525","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14052-5_13","type":"book-chapter","created":{"date-parts":[[2010,7,12]],"date-time":"2010-07-12T14:23:14Z","timestamp":1278944594000},"page":"163-178","source":"Crossref","is-referenced-by-count":34,"title":["An Efficient Coq Tactic for Deciding Kleene Algebras"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Braibant","sequence":"first","affiliation":[]},{"given":"Damien","family":"Pous","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","volume-title":"The Design and Analysis of Computer Algorithms","author":"A.V. Aho","year":"1974","unstructured":"Aho, A.V., Hopcroft, J.E., Ullman, J.D.: The Design and Analysis of Computer Algorithms. Addison-Wesley, Reading (1974)"},{"key":"13_CR2","first-page":"95","volume-title":"LICS","author":"S.F. Allen","year":"1990","unstructured":"Allen, S.F., Constable, R.L., Howe, D.J., Aitken, W.E.: The semantics of reflected proof. In: LICS, pp. 95\u2013105. IEEE Computer Society, Los Alamitos (1990)"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-540-71067-7_11","volume-title":"Theorem Proving in Higher Order Logics","author":"Y. Bertot","year":"2008","unstructured":"Bertot, Y., Gonthier, G., Ould Biha, S., Pasca, I.: Canonical big operators. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 86\u2013101. Springer, Heidelberg (2008)"},{"key":"13_CR4","unstructured":"Blanqui, F., Coupet-Grimal, S., Delobel, W., Koprowski, A.: CoLoR: a Coq library on rewriting and termination (2006)"},{"key":"13_CR5","unstructured":"Braibant, T., Pous, D.: Coq library: ATBR, algebraic tools for working with binary relations (May 2009), http:\/\/sardes.inrialpes.fr\/~braibant\/atbr\/"},{"key":"13_CR6","unstructured":"Briais, S.: Coq development: Finite automata theory (July 2008), http:\/\/www.prism.uvsq.fr\/~bris\/tools\/Automata_080708.tar.gz"},{"issue":"2","key":"13_CR7","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1016\/0304-3975(93)90287-4","volume":"120","author":"A. Br\u00fcggemann-Klein","year":"1993","unstructured":"Br\u00fcggemann-Klein, A.: Regular expressions into finite automata. TCS\u00a0120(2), 197\u2013213 (1993)","journal-title":"TCS"},{"key":"13_CR8","unstructured":"Cohen, E., Kozen, D., Smith, F.: The complexity of Kleene algebra with tests, TR96-1598, CS Dpt., Cornell University (July 1996)"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"Conchon, S., Filli\u00e2tre, J.-C.: A Persistent Union-Find Data Structure. In: ACM SIGPLAN Workshop on ML, Freiburg, Germany, October 2007, pp. 37\u201345 (2007)","DOI":"10.1145\/1292535.1292541"},{"key":"13_CR10","volume-title":"Introduction to Algorithms","author":"T.H. Cormen","year":"2001","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 2nd edn. MIT Press, Cambridge (2001)","edition":"2"},{"issue":"1-2","key":"13_CR11","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/S0304-3975(96)00154-5","volume":"179","author":"H. Doornbos","year":"1997","unstructured":"Doornbos, H., Backhouse, R., van der Woude, J.: A calculational approach to mathematical induction. TCS\u00a0179(1-2), 103\u2013135 (1997)","journal-title":"TCS"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1007\/978-3-642-03359-9_23","volume-title":"TPHOL","author":"F. Garillot","year":"2009","unstructured":"Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging mathematical structures. In: Urban, C. (ed.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 327\u2013342. Springer, Heidelberg (2009)"},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-540-74591-4_8","volume-title":"Theorem Proving in Higher Order Logics","author":"G. Gonthier","year":"2007","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.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 86\u2013101. Springer, Heidelberg (2007)"},{"key":"13_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1007\/11541868_7","volume-title":"Theorem Proving in Higher Order Logics","author":"B. Gr\u00e9goire","year":"2005","unstructured":"Gr\u00e9goire, B., Mahboubi, A.: Proving equalities in a commutative ring done right in Coq. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 98\u2013113. Springer, Heidelberg (2005)"},{"key":"13_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-540-73595-3_19","volume-title":"Automated Deduction \u2013 CADE-21","author":"P. H\u00f6fner","year":"2007","unstructured":"H\u00f6fner, P., Struth, G.: Automated reasoning in Kleene algebra. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 279\u2013294. Springer, Heidelberg (2007)"},{"key":"13_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-540-71070-7_5","volume-title":"Automated Reasoning","author":"P. H\u00f6fner","year":"2008","unstructured":"H\u00f6fner, P., Struth, G.: On automating the calculus of relations. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 50\u201366. Springer, Heidelberg (2008)"},{"issue":"1","key":"13_CR17","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1016\/S0890-5401(03)00090-7","volume":"186","author":"L. Ilie","year":"2003","unstructured":"Ilie, L., Yu, S.: Follow automata. Inf. and Comp.\u00a0186(1), 140\u2013162 (2003)","journal-title":"Inf. and Comp."},{"key":"13_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"178","DOI":"10.1007\/978-3-540-24771-5_16","volume-title":"Relational and Kleene-Algebraic Methods in Computer Science","author":"W. Kahl","year":"2004","unstructured":"Kahl, W.: Calculational relation-algebraic proofs in Isabelle\/Isar. In: Berghammer, R., M\u00f6ller, B., Struth, G. (eds.) RelMiCS 2003. LNCS, vol.\u00a03051, pp. 178\u2013190. Springer, Heidelberg (2004)"},{"key":"13_CR19","first-page":"3","volume-title":"Automata Studies","author":"S.C. Kleene","year":"1956","unstructured":"Kleene, S.C.: Representation of events in nerve nets and finite automata. In: Automata Studies, pp. 3\u201341. Princeton University Press, Princeton (1956)"},{"issue":"2","key":"13_CR20","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1006\/inco.1994.1037","volume":"110","author":"D. Kozen","year":"1994","unstructured":"Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Inf. and Comp.\u00a0110(2), 366\u2013390 (1994)","journal-title":"Inf. and Comp."},{"key":"13_CR21","unstructured":"Kozen, D.: Typed Kleene algebra, TR98-1669, CS Dpt. Cornell University (1998)"},{"issue":"1","key":"13_CR22","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1145\/343369.343378","volume":"1","author":"D. Kozen","year":"2000","unstructured":"Kozen, D.: On Hoare logic and Kleene algebra with tests. ACM Trans. Comput. Log.\u00a01(1), 60\u201376 (2000)","journal-title":"ACM Trans. Comput. Log."},{"key":"13_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1007\/3-540-63172-0_43","volume-title":"Computer Science Logic","author":"D. Kozen","year":"1997","unstructured":"Kozen, D., Smith, F.: Kleene algebra with tests: Completeness and decidability. In: van Dalen, D., Bezem, M. (eds.) CSL 1996. LNCS, vol.\u00a01258, pp. 244\u2013259. Springer, Heidelberg (1997)"},{"issue":"2","key":"13_CR24","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1016\/0304-3975(91)90395-I","volume":"89","author":"D. Krob","year":"1991","unstructured":"Krob, D.: Complete systems of B-rational identities. TCS\u00a089(2), 207\u2013343 (1991)","journal-title":"TCS"},{"issue":"4","key":"13_CR25","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","volume":"43","author":"X. Leroy","year":"2009","unstructured":"Leroy, X.: A formally verified compiler back-end. JAR\u00a043(4), 363\u2013446 (2009)","journal-title":"JAR"},{"key":"13_CR26","first-page":"1","volume-title":"Proc. STOC","author":"A.R. Meyer","year":"1973","unstructured":"Meyer, A.R., Stockmeyer, L.J.: Word problems requiring exponential time. In: Proc. STOC, pp. 1\u20139. ACM, New York (1973)"},{"key":"13_CR27","unstructured":"Narboux, J.: Formalisation et automatisation du raisonnement g\u00e9om\u00e9trique en Coq. PhD thesis, Universit\u00e9 Paris Sud (September 2006)"},{"key":"13_CR28","doi-asserted-by":"crossref","unstructured":"Pous, D.: Untyping typed algebraic structures and colouring proof nets of cyclic linear logic. Technical Report RR-7176, INRIA Rh\u00f4ne-Alpes (January 2010)","DOI":"10.1007\/978-3-642-15205-4_37"},{"issue":"2","key":"13_CR29","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1147\/rd.32.0114","volume":"3","author":"M.O. Rabin","year":"1959","unstructured":"Rabin, M.O., Scott, D.: Finite automata and their decision problems. IBM Journal of Research and Development\u00a03(2), 114\u2013125 (1959)","journal-title":"IBM Journal of Research and Development"},{"key":"13_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-540-71067-7_23","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Sozeau","year":"2008","unstructured":"Sozeau, M., Oury, N.: First-class type classes. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 278\u2013293. Springer, Heidelberg (2008)"},{"key":"13_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/3-540-36280-0_19","volume-title":"Relational Methods in Computer Science","author":"G. Struth","year":"2002","unstructured":"Struth, G.: Calculating Church-Rosser proofs in Kleene algebra. In: de Swart, H. (ed.) RelMiCS 2001. LNCS, vol.\u00a02561, pp. 276\u2013290. Springer, Heidelberg (2002)"},{"key":"13_CR32","doi-asserted-by":"crossref","unstructured":"Tarski, A., Givant, S.: A Formalization of Set Theory without Variables, AMS, Providence, Rhode Island, vol.\u00a041. Colloquium Publications (1987)","DOI":"10.1090\/coll\/041"},{"key":"13_CR33","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1145\/363347.363387","volume":"11","author":"K. Thompson","year":"1968","unstructured":"Thompson, K.: Regular expression search algorithm. ACM C.\u00a011, 419\u2013422 (1968)","journal-title":"ACM C."},{"key":"13_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"380","DOI":"10.1007\/3-540-63104-6_36","volume-title":"Automated Deduction - CADE-14","author":"D. Oheimb von","year":"1997","unstructured":"von Oheimb, D., Gritzner, T.F.: RALL: Machine-supported proofs for relation algebra. In: McCune, W. (ed.) CADE 1997. LNCS, vol.\u00a01249, pp. 380\u2013394. Springer, Heidelberg (1997)"}],"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-14052-5_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:47:00Z","timestamp":1606186020000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14052-5_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642140518","9783642140525"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14052-5_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}