{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:20:28Z","timestamp":1776316828665,"version":"3.50.1"},"reference-count":56,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,3,2]],"date-time":"2012-03-02T00:00:00Z","timestamp":1330646400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We present a reflexive tactic for deciding the equational theory of Kleene algebras in the Coq proof assistant. This tactic relies on a careful implementation of efficient finite automata algorithms, so that it solves casual equations instantaneously and properly scales to larger expressions. The decision procedure is proved correct and complete: correctness is established w.r.t. any model by formalising Kozen's initiality theorem; a counter-example is returned when the given equation does not hold. The correctness proof is challenging: it involves both a precise analysis of the underlying automata algorithms and a lot of algebraic reasoning. In particular, we have to formalise the theory of matrices over a Kleene algebra. We build on the recent addition of firstorder typeclasses in Coq in order to work efficiently with the involved algebraic structures.<\/jats:p>","DOI":"10.2168\/lmcs-8(1:16)2012","type":"journal-article","created":{"date-parts":[[2012,9,6]],"date-time":"2012-09-06T10:03:11Z","timestamp":1346925791000},"source":"Crossref","is-referenced-by-count":17,"title":["Deciding Kleene Algebras in Coq"],"prefix":"10.46298","volume":"Volume 8, Issue 1","author":[{"given":"Thomas","family":"Braibant","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1220-4399","authenticated-orcid":false,"given":"Damien","family":"Pous","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,3,2]]},"reference":[{"key":"10.2168\/LMCS-8(1:16)2012_AhoHU74","unstructured":"A. V. Aho, J. E. Hopcroft, and J. D. Ullman.The Design and Analysis of Computer Algorithms. Addison-Wesley, 1974."},{"key":"10.2168\/LMCS-8(1:16)2012_DBLP:conf\/lics\/AllenCHA90","doi-asserted-by":"crossref","unstructured":"S. F. Allen, R. L. Constable, D. J. Howe, and W. E. Aitken. The semantics of reflected proof. InLICS, pages 95-105. IEEE Computer Society, 1990.","DOI":"10.1109\/LICS.1990.113737"},{"key":"10.2168\/LMCS-8(1:16)2012_ArmandGST10","doi-asserted-by":"crossref","unstructured":"M. Armand, B. Gr\u00e9goire, A. Spiwack, and L. Th\u00e9ry. Extending Coq with imperative features and its application to SAT verification. InProc. ITP, volume 6172 ofLecture Notes in Computer Science, pages 83-98. Springer Verlag, 2010.","DOI":"10.1007\/978-3-642-14052-5_8"},{"key":"10.2168\/LMCS-8(1:16)2012_Barthe95","doi-asserted-by":"crossref","unstructured":"G. Barthe. Implicit coercions in type systems. InTYPES, volume 1158 ofLecture Notes in Computer Science, pages 1-15. Springer Verlag, 1995.","DOI":"10.1007\/3-540-61780-9_58"},{"key":"10.2168\/LMCS-8(1:16)2012_BertotGBP08","doi-asserted-by":"crossref","unstructured":"Y. Bertot, G. Gonthier, S. Ould Biha, and I. Pasca. Canonical big operators. InProc. TPHOL, volume 5170 ofLecture Notes in Computer Science, pages 86-101. Springer Verlag, 2008.","DOI":"10.1007\/978-3-540-71067-7_11"},{"key":"10.2168\/LMCS-8(1:16)2012_bt95","unstructured":"G. Betarte and A. Tasistro. Formalisation of systems of algebras using dependent record types and subtyping: an example. InProc. 7th Nordic workshop on Pro- gramming Theory, 1995."},{"key":"10.2168\/LMCS-8(1:16)2012_color","unstructured":"F. Blanqui, S. Coupet-Grimal, W. Delobel, and A. Koprowski. CoLoR: a Coq library on rewriting and termination, 2006. R. Boyer and J. Moore. Metafunctions: proving them correct and using them efficiently as new proof procedures. InThe Correctness Problem in Computer Science. NY: Academic Press, 1981."},{"key":"10.2168\/LMCS-8(1:16)2012_kleenecoq:web","unstructured":"T. Braibant and D. Pous. Coq library: ATBR, algebraic tools for working with binary relations. http:\/\/sardes.inrialpes.fr\/ braibant\/atbr\/, May 2009."},{"key":"10.2168\/LMCS-8(1:16)2012_BraibantP10","doi-asserted-by":"crossref","unstructured":"T. Braibant and D. Pous. An efficient Coq tactic for deciding Kleene algebras. InProc. ITP, volume 6172 ofLecture Notes in Computer Science, pages 163-178. Springer Verlag, 2010.","DOI":"10.1007\/978-3-642-14052-5_13"},{"key":"10.2168\/LMCS-8(1:16)2012_grosquick","unstructured":"S. Briais. Coq development: Finite automata theory. http:\/\/www.prism.uvsq.fr\/ bris\/tools\/Automatan080708.tar.gz, July 2008."},{"issue":"2","key":"10.2168\/LMCS-8(1:16)2012_klein93","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1016\/0304-3975(93)90287-4","volume":"120","author":"A. Br\u00fcggemann-Klein","year":"1993","journal-title":"Theoretical Computer Science"},{"issue":"4","key":"10.2168\/LMCS-8(1:16)2012_Brzozowski64","doi-asserted-by":"crossref","first-page":"481","DOI":"10.1145\/321239.321249","volume":"11","author":"J. A. Brzozowski","year":"1964","journal-title":"J. ACM"},{"key":"10.2168\/LMCS-8(1:16)2012_CoenT07","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68103-8_11"},{"key":"10.2168\/LMCS-8(1:16)2012_CoenT09","doi-asserted-by":"crossref","unstructured":"C. Sacerdoti Coen and E. Tassi. Nonuniform coercions via unification hints. InProc. TYPES, volume 53 ofEPTCS, pages 16-29, 2009.","DOI":"10.4204\/EPTCS.53.2"},{"key":"10.2168\/LMCS-8(1:16)2012_KATComplexity","unstructured":"E. Cohen, D. Kozen, and F. Smith. The complexity of Kleene algebra with tests, 1996. TR96-1598, CS Dpt., Cornell University."},{"key":"10.2168\/LMCS-8(1:16)2012_persistant_union_find","doi-asserted-by":"crossref","unstructured":"S. Conchon and J.-C. Filliatre. A Persistent Union-Find Data Structure. InProc. ACM SIGPLAN Workshop on ML, pages 37-45, Freiburg, Germany, October 2007.","DOI":"10.1145\/1292535.1292541"},{"key":"10.2168\/LMCS-8(1:16)2012_CoquandS11","doi-asserted-by":"crossref","unstructured":"T. Coquand and V. Siles. A decision procedure for regular expression equivalence in type theory. InProc. CPP, volume 7086 ofLecture Notes in Computer Science, pages 119-134. Springer Verlag, 2011.","DOI":"10.1007\/978-3-642-25379-9_11"},{"key":"10.2168\/LMCS-8(1:16)2012_cormen_introduction_2001","unstructured":"T. H. Cormen, C. E. Leiserson, R. L. Rivest, and C. Stein.Introduction to Algorithms. MIT Press, Cambridge, MA, second edition, 2001."},{"issue":"1-2","key":"10.2168\/LMCS-8(1:16)2012_CrvenkovicDE00","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1016\/S0304-3975(99)00079-1","volume":"230","author":"S. Crvenkovic, I. Dolinka, and Z. \u00c9sik","year":"2000","journal-title":"Theoretical Computer Science"},{"key":"10.2168\/LMCS-8(1:16)2012_DaveyPriestley90","unstructured":"Brian Davey and Hilary Priestley.Introduction to Lattices and Order. Cambridge University Press, 1990."},{"issue":"1-2","key":"10.2168\/LMCS-8(1:16)2012_DBW97","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1016\/S0304-3975(96)00154-5","volume":"179","author":"H. Doornbos, R. Backhouse, and J. van de","year":"1997","journal-title":"Theoretical Computer Science"},{"key":"10.2168\/LMCS-8(1:16)2012_FosterSW11","doi-asserted-by":"crossref","unstructured":"S. Foster, G. Struth, and T. Weber. Automated engineering of relational and algebraic methods in Isabelle\/HOL - (invited tutorial). InProc. RAMICS, volume 6663 ofLecture Notes in Computer Science, pages 52-67. Springer Verlag, 2011.","DOI":"10.1007\/978-3-642-21070-9_5"},{"key":"10.2168\/LMCS-8(1:16)2012_FreydScedrov90","unstructured":"P. Freyd and A. Scedrov.Categories, Allegories. North Holland, 1990."},{"key":"10.2168\/LMCS-8(1:16)2012_pack:math:struct","doi-asserted-by":"crossref","unstructured":"F. Garillot, G. Gonthier, A. Mahboubi, and L. Rideau. Packaging mathematical structures. InProc. TPHOL, volume 5674 ofLecture Notes in Computer Science, pages 327-342. Springer Verlag, 2009.","DOI":"10.1007\/978-3-642-03359-9_23"},{"issue":"4","key":"10.2168\/LMCS-8(1:16)2012_GeuversPWZ02","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1006\/jsco.2002.0552","volume":"34","author":"H. Geuvers, R. Pollack, F. Wiedijk, and","year":"2002","journal-title":"Journal of Symbolic Computation"},{"key":"10.2168\/LMCS-8(1:16)2012_gonthier:itp11","doi-asserted-by":"crossref","unstructured":"G. Gonthier. Point-free, set-free concrete linear algebra. InProc. ITP, volume 6898 ofLecture Notes in Computer Science, pages 103-118. Springer Verlag, 2011.","DOI":"10.1007\/978-3-642-22863-6_10"},{"key":"10.2168\/LMCS-8(1:16)2012_GregoireL02","doi-asserted-by":"crossref","unstructured":"B. Gr\u00e9goire and X. Leroy. A compiled implementation of strong reduction. InProc. ICFP, pages 235-246, 2002.","DOI":"10.1145\/583852.581501"},{"key":"10.2168\/LMCS-8(1:16)2012_DBLP:conf\/tphol\/GregoireM05","doi-asserted-by":"crossref","unstructured":"B. Gr\u00e9goire and A. Mahboubi. Proving equalities in a commutative ring done right in Coq. InTPHOL, volume 3603 ofLecture Notes in Computer Science, pages 98-113. Springer Verlag, 2005.","DOI":"10.1007\/11541868_7"},{"issue":"4","key":"10.2168\/LMCS-8(1:16)2012_Hedberg98","doi-asserted-by":"crossref","first-page":"413","DOI":"10.1017\/S0956796898003153","volume":"8","author":"M. Hedberg","year":"1998","journal-title":"J. of Functional Programming"},{"key":"10.2168\/LMCS-8(1:16)2012_StruthHofner_KA","doi-asserted-by":"crossref","unstructured":"P. H\u00f6fner and G. Struth. Automated reasoning in Kleene algebra. InProc. CADE, volume 4603 ofLecture Notes in Computer Science, pages 279-294. Springer Verlag, 2007.","DOI":"10.1007\/978-3-540-73595-3_19"},{"key":"10.2168\/LMCS-8(1:16)2012_DBLP:conf\/cade\/HofnerS08","doi-asserted-by":"crossref","unstructured":"P. H\u00f6fner and G. Struth. On automating the calculus of relations. InIJCAR, volume 5195 ofLecture Notes in Computer Science, pages 50-66. Springer Verlag, 2008.","DOI":"10.1007\/978-3-540-71070-7_5"},{"key":"10.2168\/LMCS-8(1:16)2012_HopcroftKarp","unstructured":"J. E. Hopcroft and R. M. Karp. A linear algorithm for testing equivalence of finite automata. Technical Report 114, Cornell University, December 1971."},{"issue":"1","key":"10.2168\/LMCS-8(1:16)2012_Ilie-yu-FollowAutomata","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1016\/S0890-5401(03)00090-7","volume":"186","author":"L. Ilie and S. Yu","year":"2003","journal-title":"Information and Computation"},{"issue":"2","key":"10.2168\/LMCS-8(1:16)2012_Jipsen04","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1023\/B:STUD.0000032089.54776.63","volume":"76","author":"P. Jipsen","year":"2004","journal-title":"Studia Logica"},{"key":"10.2168\/LMCS-8(1:16)2012_Kahl-ISAR","doi-asserted-by":"crossref","unstructured":"W. Kahl. Calculational relation-algebraic proofs in Isabelle\/Isar. InProc. RelMiCS, volume 3051 ofLecture Notes in Computer Science, pages 178-190. Springer Verlag, 2003.","DOI":"10.1007\/978-3-540-24771-5_16"},{"key":"10.2168\/LMCS-8(1:16)2012_Kle56","doi-asserted-by":"crossref","unstructured":"S. C. Kleene. Representation of events in nerve nets and finite automata. InAutomata Studies, pages 3-41. Princeton University Press, 1956.","DOI":"10.1515\/9781400882618-002"},{"issue":"2","key":"10.2168\/LMCS-8(1:16)2012_Koz94b","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1006\/inco.1994.1037","volume":"110","author":"D. Kozen","year":"1994","journal-title":"Information and Computation"},{"key":"10.2168\/LMCS-8(1:16)2012_Koz98b","author":"D. Kozen","journal-title":"TR98-1669, CS Dpt. Cornell University"},{"issue":"1","key":"10.2168\/LMCS-8(1:16)2012_kozen:hoare:kat:00","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1145\/343369.343378","volume":"1","author":"D. Kozen","year":"2000","journal-title":"ACM Trans. Comput. Log."},{"key":"10.2168\/LMCS-8(1:16)2012_KATCompletenessDecidability","doi-asserted-by":"crossref","unstructured":"D. Kozen and F. Smith. Kleene algebra with tests: Completeness and decidability. InCSL, volume 1258 ofLecture Notes in Computer Science, pages 244-259. Springer Verlag, September 1996.","DOI":"10.1007\/3-540-63172-0_43"},{"key":"10.2168\/LMCS-8(1:16)2012_Krauss","doi-asserted-by":"crossref","unstructured":"A. Krauss and T. Nipkow. Proof pearl: Regular expression equivalence and relation algebra, 2011. To appear in J. of Algebraic Reasoning.","DOI":"10.1007\/s10817-011-9223-4"},{"issue":"2","key":"10.2168\/LMCS-8(1:16)2012_Krob91a","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1016\/0304-3975(91)90395-I","volume":"89","author":"D. Krob","year":"1991","journal-title":"Theoretical Computer Science"},{"issue":"4","key":"10.2168\/LMCS-8(1:16)2012_Leroy-backend","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","volume":"43","author":"X. Leroy","year":"2009","journal-title":"J. of Algebraic Reasoning"},{"key":"10.2168\/LMCS-8(1:16)2012_Maclane:cwm","unstructured":"Saunders Mac Lane.Categories for the Working Mathematician. Number 5 in Graduate Texts in Mathematics. Springer Verlag, 2nd edition, 1998."},{"key":"10.2168\/LMCS-8(1:16)2012_MS73","doi-asserted-by":"crossref","unstructured":"A.R. Meyer and L. J. Stockmeyer. Word problems requiring exponential time. InProc. STOC, pages 1-9. ACM, 1973.","DOI":"10.1145\/800125.804029"},{"key":"10.2168\/LMCS-8(1:16)2012_narbouxPhD","unstructured":"J. Narboux.Formalisation et automatisation du raisonnement geom\u00e9trique en Coq. PhD thesis, Universit\u00e9 Paris Sud, September 2006."},{"key":"10.2168\/LMCS-8(1:16)2012_pous:csl10:utas","doi-asserted-by":"crossref","unstructured":"D. Pous. Untyping typed algebraic structures and colouring proof nets of cyclic linear logic. InProc. CSL, volume 6247 ofLecture Notes in Computer Science, pages 484-498. Springer Verlag, August 2010.","DOI":"10.1007\/978-3-642-15205-4_37"},{"issue":"2","key":"10.2168\/LMCS-8(1:16)2012_RabinScott","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1147\/rd.32.0114","volume":"3","author":"M.O. Rabin and D. Scott","year":"1959","journal-title":"IBM Journal of Research and Development"},{"key":"10.2168\/LMCS-8(1:16)2012_redko64","first-page":"120","volume":"16","author":"V. Redko","year":"1964","journal-title":"Ukrain. Mat. Z."},{"key":"10.2168\/LMCS-8(1:16)2012_Rutten98","doi-asserted-by":"crossref","unstructured":"J. J. M. M. Rutten. Automata and coinduction (an exercise in coalgebra). InProc. CONCUR, volume 1466 ofLecture Notes in Computer Science, pages 194-218. Springer Verlag, 1998.","DOI":"10.1007\/BFb0055624"},{"key":"10.2168\/LMCS-8(1:16)2012_SozeauOury08","doi-asserted-by":"crossref","unstructured":"M. Sozeau and N. Oury. First-class type classes. InProc. TPHOL, volume 4732 ofLecture Notes in Computer Science, pages 278-293. Springer Verlag, 2008.","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"10.2168\/LMCS-8(1:16)2012_math-classes","unstructured":"B. Spitters and E. van der Weegen. Type classes for mathematics in type theory.MSCS, special issue on `Interactive theorem proving and the formalization of mathematics', 21:1-31, 2011. (A four pages abstract appeared in Proc. ITP 2010.)."},{"key":"10.2168\/LMCS-8(1:16)2012_Struth-ChurchRosser-KleeneAlgebra","doi-asserted-by":"crossref","unstructured":"G. Struth. Calculating Church-Rosser proofs in Kleene algebra. InProc. RelMiCS, volume 2561 ofLecture Notes in Computer Science, pages 276-290. Springer Verlag, 2001.","DOI":"10.1007\/3-540-36280-0_19"},{"key":"10.2168\/LMCS-8(1:16)2012_TG87","doi-asserted-by":"crossref","unstructured":"A. Tarski and S. Givant.A Formalization of Set Theory without Variables, volume 41 ofColloquium Publications. American Mathematical Society, Providence, Rhode Island, 1987.","DOI":"10.1090\/coll\/041"},{"key":"10.2168\/LMCS-8(1:16)2012_thompson68","doi-asserted-by":"crossref","first-page":"419","DOI":"10.1145\/363347.363387","volume":"11","author":"K. Thompson","year":"1968","journal-title":"C. ACM"},{"key":"10.2168\/LMCS-8(1:16)2012_RALL","doi-asserted-by":"crossref","unstructured":"D. von Oheimb and T.F. Gritzner. RALL: Machine-supported proofs for relation algebra. InProc. CADE, volume 1249 ofLecture Notes in Computer Science, pages 380-394. Springer Verlag, 1997.","DOI":"10.1007\/3-540-63104-6_36"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1043\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1043\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,7]],"date-time":"2025-04-07T23:09:54Z","timestamp":1744067394000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1043"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,3,2]]},"references-count":56,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(1:16)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1105.4537","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1105.4537","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,3,2]]},"article-number":"1043"}}