{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,3]],"date-time":"2026-03-03T00:48:34Z","timestamp":1772498914502,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642396335","type":"print"},{"value":"9783642396342","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39634-2_15","type":"book-chapter","created":{"date-parts":[[2013,7,22]],"date-time":"2013-07-22T09:52:36Z","timestamp":1374486756000},"page":"180-196","source":"Crossref","is-referenced-by-count":24,"title":["Kleene Algebra with Tests and Coq Tools for while Programs"],"prefix":"10.1007","author":[{"given":"Damien","family":"Pous","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","unstructured":"Allen, S.F., Constable, R.L., Howe, D.J., Aitken, W.E.: The semantics of reflected proof. In: Proc. LICS, pp. 95\u2013105. IEEE Computer Society (1990)"},{"key":"15_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-3-642-18098-9_7","volume-title":"Implementation and Application of Automata","author":"J.B. Almeida","year":"2011","unstructured":"Almeida, J.B., Moreira, N., Pereira, D., de Sousa, S.M.: Partial derivative automata formalized in Coq. In: Domaratzki, M., Salomaa, K. (eds.) CIAA 2010. LNCS, vol.\u00a06482, pp. 59\u201368. Springer, Heidelberg (2011)"},{"key":"15_CR3","unstructured":"Angus, A., Kozen, D.: Kleene algebra with tests and program schematology. Technical Report TR2001-1844, CS Dpt, Cornell University (July 2001)"},{"issue":"2","key":"15_CR4","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/0304-3975(95)00182-4","volume":"155","author":"V.M. Antimirov","year":"1996","unstructured":"Antimirov, V.M.: Partial derivatives of regular expressions and finite automaton constructions. TCS\u00a0155(2), 291\u2013319 (1996)","journal-title":"TCS"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-642-33314-9_5","volume-title":"Relational and Algebraic Methods in Computer Science","author":"A. Armstrong","year":"2012","unstructured":"Armstrong, A., Struth, G.: Automated reasoning in higher-order regular algebra. In: Kahl, W., Griffin, T.G. (eds.) RAMICS 2012. LNCS, vol.\u00a07560, pp. 66\u201381. Springer, Heidelberg (2012)"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/978-3-642-32347-8_19","volume-title":"Interactive Theorem Proving","author":"A. Asperti","year":"2012","unstructured":"Asperti, A.: A compact proof of decidability for regular expression equivalence. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol.\u00a07406, pp. 283\u2013298. Springer, Heidelberg (2012)"},{"key":"15_CR7","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., Biha, S.O., 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":"15_CR8","unstructured":"Boyer, R., Moore, J.: Metafunctions: proving them correct and using them efficiently as new proof procedures. In: The Correctness Problem in Computer Science. Academic Press, NY (1981)"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-642-14052-5_13","volume-title":"Interactive Theorem Proving","author":"T. Braibant","year":"2010","unstructured":"Braibant, T., Pous, D.: An efficient Coq tactic for deciding Kleene algebras. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 163\u2013178. Springer, Heidelberg (2010)"},{"issue":"4","key":"15_CR10","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1145\/321239.321249","volume":"11","author":"J.A. Brzozowski","year":"1964","unstructured":"Brzozowski, J.A.: Derivatives of regular expressions. J. ACM\u00a011(4), 481\u2013494 (1964)","journal-title":"J. ACM"},{"key":"15_CR11","unstructured":"Cohen, E.: Hypotheses in Kleene algebra. Technical report, Bellcore, Morristown, N.J (1994)"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-642-25379-9_11","volume-title":"Certified Programs and Proofs","author":"T. Coquand","year":"2011","unstructured":"Coquand, T., Siles, V.: A decision procedure for regular expression equivalence in type theory. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol.\u00a07086, pp. 119\u2013134. Springer, Heidelberg (2011)"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-642-31365-3_22","volume-title":"Automated Reasoning","author":"S. Foster","year":"2012","unstructured":"Foster, S., Struth, G.: Automated analysis of regular algebra. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol.\u00a07364, pp. 271\u2013285. Springer, Heidelberg (2012)"},{"key":"15_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"15_CR15","unstructured":"Hardin, C., Kozen, D.: On the elimination of hypotheses in Kleene algebra with tests. Technical Report TR2002-1879, CS Dpt, Cornell University (October 2002)"},{"issue":"10","key":"15_CR16","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM\u00a012(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"Komendantsky, V.: Reflexive toolbox for regular expression matching: verification of functional programs in Coq+ssreflect. In: Proc. PLPV, pp. 61\u201370. ACM (2012)","DOI":"10.1145\/2103776.2103784"},{"issue":"2","key":"15_CR18","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."},{"issue":"3","key":"15_CR19","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1145\/256167.256195","volume":"19","author":"D. Kozen","year":"1997","unstructured":"Kozen, D.: Kleene algebra with tests. Transactions on Programming Languages and Systems\u00a019(3), 427\u2013443 (1997)","journal-title":"Transactions on Programming Languages and Systems"},{"key":"15_CR20","unstructured":"Kozen, D.: Typed Kleene algebra, TR98-1669, CS Dpt. Cornell University (1998)"},{"issue":"1","key":"15_CR21","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":"15_CR22","unstructured":"Kozen, D.: On the coalgebraic theory of Kleene algebra with tests. Technical Report\u00a0 CIS, Cornell University (March 2008), \n                    \n                      http:\/\/hdl.handle.net\/1813\/10173"},{"key":"15_CR23","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"568","DOI":"10.1007\/3-540-44957-4_38","volume-title":"Computational Logic - CL 2000","author":"D. Kozen","year":"2000","unstructured":"Kozen, D., Patron, M.-C.: Certification of compiler optimizations using Kleene algebra with tests. In: Palamidessi, C., et al. (eds.) CL 2000. LNCS (LNAI), vol.\u00a01861, pp. 568\u2013582. Springer, Heidelberg (2000)"},{"key":"15_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"1","key":"15_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. JAR\u00a049(1), 95\u2013106 (2012)","journal-title":"JAR"},{"key":"15_CR26","unstructured":"Manna, Z.: Mathematical Theory of Computation. McGraw-Hill (1974)"},{"key":"15_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-642-33314-9_7","volume-title":"Relational and Algebraic Methods in Computer Science","author":"N. Moreira","year":"2012","unstructured":"Moreira, N., Pereira, D., de Sousa, S.M.: Deciding regular expressions (In-) equivalence in Coq. In: Kahl, W., Griffin, T.G. (eds.) RAMICS 2012. LNCS, vol.\u00a07560, pp. 98\u2013113. Springer, Heidelberg (2012)"},{"issue":"2","key":"15_CR28","doi-asserted-by":"publisher","first-page":"137","DOI":"10.2298\/CSIS0802137P","volume":"5","author":"D. Pereira","year":"2008","unstructured":"Pereira, D., Moreira, N.: KAT and PHL in Coq. Comput. Sci. Inf. Syst.\u00a05(2), 137\u2013160 (2008)","journal-title":"Comput. Sci. Inf. Syst."},{"key":"15_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1007\/978-3-642-15205-4_37","volume-title":"Computer Science Logic","author":"D. Pous","year":"2010","unstructured":"Pous, D.: Untyping typed algebraic structures and colouring proof nets of cyclic linear logic. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol.\u00a06247, pp. 484\u2013498. Springer, Heidelberg (2010)"},{"key":"15_CR30","unstructured":"Pous, D.: RelationAlgebra: Coq library containing all material presented in this paper (December 2012), \n                    \n                      http:\/\/perso.ens-lyon.fr\/damien.pous\/ra"},{"key":"15_CR31","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. C. ACM\u00a011, 419\u2013422 (1968)","journal-title":"C. ACM"}],"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-39634-2_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T22:15:42Z","timestamp":1557958542000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39634-2_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642396335","9783642396342"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39634-2_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}