{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,7]],"date-time":"2025-12-07T14:10:25Z","timestamp":1765116625287,"version":"3.46.0"},"publisher-location":"Cham","reference-count":54,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031995354"},{"type":"electronic","value":"9783031995361"}],"license":[{"start":{"date-parts":[[2025,8,1]],"date-time":"2025-08-01T00:00:00Z","timestamp":1754006400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,8,1]],"date-time":"2025-08-01T00:00:00Z","timestamp":1754006400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-031-99536-1_1","type":"book-chapter","created":{"date-parts":[[2025,7,31]],"date-time":"2025-07-31T10:54:05Z","timestamp":1753959245000},"page":"3-18","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["On Propositional Program Equivalence (Extended Abstract)"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6068-880X","authenticated-orcid":false,"given":"Tobias","family":"Kapp\u00e9","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,8,1]]},"reference":[{"key":"1_CR1","doi-asserted-by":"publisher","unstructured":"Azevedo de Amorim, A., Zhang, C., Gaboardi, M.: Kleene algebra with commutativity conditions is undecidable. In: CSL, pp. 36:1\u201336:25 (2025). https:\/\/doi.org\/10.4230\/LIPICS.CSL.2025.36","DOI":"10.4230\/LIPICS.CSL.2025.36"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Benevides, M., Gomes, L., Lopes, B.: Towards determinism in PDL: relations and proof theory. J. Logic Comput., exae022 (2024)","DOI":"10.1093\/logcom\/exae022"},{"key":"1_CR3","unstructured":"Birkhoff, G., Bartee, T.C.: Modern Applied Algebra. McGraw-Hill, Boston (1970)"},{"key":"1_CR4","doi-asserted-by":"publisher","unstructured":"ten Cate, B., Kapp\u00e9, T.: Algebras for deterministic computation are inherently incomplete. In: POPL, pp. 25:1\u201325:27 (2025). https:\/\/doi.org\/10.1145\/3704861","DOI":"10.1145\/3704861"},{"issue":"1\u20132","key":"1_CR5","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/j.tcs.2004.07.020","volume":"327","author":"H Chen","year":"2004","unstructured":"Chen, H., Pucella, R.: A coalgebraic approach to Kleene algebra with tests. Theor. Comput. Sci. 327(1\u20132), 23\u201344 (2004). https:\/\/doi.org\/10.1016\/j.tcs.2004.07.020","journal-title":"Theor. Comput. Sci."},{"key":"1_CR6","unstructured":"Cifuentes, C.: Reverse compilation techniques. Ph.D. thesis, Queensland University of Technology (1994)"},{"key":"1_CR7","unstructured":"Cohen, E.: Hypotheses in Kleene algebra. Technical report, Bellcore (1994)"},{"key":"1_CR8","unstructured":"Cohen, E., Kozen, D., Smith, F.: The complexity of Kleene algebra with tests. Technical Report. TR96-1598, Cornell University (1996)"},{"key":"1_CR9","volume-title":"Regular Algebra and Finite Machines","author":"JH Conway","year":"1971","unstructured":"Conway, J.H.: Regular Algebra and Finite Machines. Chapman and Hall Ltd., London (1971)"},{"key":"1_CR10","doi-asserted-by":"publisher","unstructured":"Dahlqvist, F., Schmid, T.: How to write a coequation ((co)algebraic pearls). In: CALCO, pp. 13:1\u201313:25 (2021). https:\/\/doi.org\/10.4230\/LIPICS.CALCO.2021.13","DOI":"10.4230\/LIPICS.CALCO.2021.13"},{"issue":"4","key":"1_CR11","doi-asserted-by":"publisher","first-page":"798","DOI":"10.1145\/1183278.1183285","volume":"7","author":"J Desharnais","year":"2006","unstructured":"Desharnais, J., M\u00f6ller, B., Struth, G.: Kleene algebra with domain. ACM Trans. Comput. Log. 7(4), 798\u2013833 (2006). https:\/\/doi.org\/10.1145\/1183278.1183285","journal-title":"ACM Trans. Comput. Log."},{"issue":"3","key":"1_CR12","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1145\/362929.362947","volume":"11","author":"EW Dijkstra","year":"1968","unstructured":"Dijkstra, E.W.: Letters to the editor: go to statement considered harmful. Commun. ACM 11(3), 147\u2013148 (1968). https:\/\/doi.org\/10.1145\/362929.362947","journal-title":"Commun. ACM"},{"key":"1_CR13","unstructured":"Dijkstra, E.W.: On a somewhat disappointing correspondence (1987). http:\/\/www.cs.utexas.edu\/users\/EWD\/ewd10xx\/EWD1009.PDF"},{"key":"1_CR14","doi-asserted-by":"publisher","unstructured":"Doumane, A., Kuperberg, D., Pous, D., Pradic, P.: Kleene algebra with hypotheses. In: FoSSaCS, pp. 207\u2013223 (2019). https:\/\/doi.org\/10.1007\/978-3-030-17127-8_12","DOI":"10.1007\/978-3-030-17127-8_12"},{"issue":"2","key":"1_CR15","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1017\/S096012950400458X","volume":"15","author":"R Goldblatt","year":"2005","unstructured":"Goldblatt, R.: A comonadic account of behavioural covarieties of coalgebras. Math. Struct. Comput. Sci. 15(2), 243\u2013269 (2005). https:\/\/doi.org\/10.1017\/S096012950400458X","journal-title":"Math. Struct. Comput. Sci."},{"key":"1_CR16","doi-asserted-by":"publisher","unstructured":"Gomes, L., Baillot, P., Gaboardi, M.: BiGKAT: an algebraic framework for relational verification of probabilistic programs. In: FoSSaCS, pp. 243\u2013264 (2025). https:\/\/doi.org\/10.1007\/978-3-031-90897-2_12","DOI":"10.1007\/978-3-031-90897-2_12"},{"key":"1_CR17","doi-asserted-by":"publisher","unstructured":"Grabmayer, C.: Milner\u2019s proof system for regular expressions modulo bisimilarity is complete. In: LICS, pp. 34:1\u201334:13. ACM (2022). https:\/\/doi.org\/10.1145\/3531130.3532430. https:\/\/arxiv.org\/abs\/2209.12188","DOI":"10.1145\/3531130.3532430"},{"key":"1_CR18","doi-asserted-by":"publisher","unstructured":"Grabmayer, C., Fokkink, W.J.: A complete proof system for 1-free regular expressions modulo bisimilarity. In: LICS, pp. 465\u2013478. ACM (2020). https:\/\/doi.org\/10.1145\/3373718.3394744","DOI":"10.1145\/3373718.3394744"},{"key":"1_CR19","unstructured":"Hardin, C.: The Horn theory of relational Kleene algebra. Ph.D. thesis, Cornell University (2005)"},{"key":"1_CR20","unstructured":"Hopcroft, J.E., Karp, R.M.: A linear algorithm for testing equivalence of finite automata. Technical Report. TR71-114, Cornell University (1971)"},{"key":"1_CR21","doi-asserted-by":"publisher","unstructured":"Jacobs, B.: A bialgebraic review of deterministic automata, regular expressions and languages. In: Algebra, Meaning, and Computation, Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday, pp. 375\u2013404 (2006). https:\/\/doi.org\/10.1007\/11780274_20","DOI":"10.1007\/11780274_20"},{"key":"1_CR22","doi-asserted-by":"publisher","unstructured":"Kapp\u00e9, T., Brunet, P., Silva, A., Wagemaker, J., Zanasi, F.: Concurrent Kleene algebra with observations: from hypotheses to completeness. In: FoSSaCS, pp. 381\u2013400 (2020). https:\/\/doi.org\/10.1007\/978-3-030-45231-5_20","DOI":"10.1007\/978-3-030-45231-5_20"},{"key":"1_CR23","doi-asserted-by":"publisher","unstructured":"Kapp\u00e9, T., Schmid, T.: A general completeness theorem for skip-free star algebras. In: FoSSaCS, pp. 265\u2013286 (2025). https:\/\/doi.org\/10.1007\/978-3-031-90897-2_13","DOI":"10.1007\/978-3-031-90897-2_13"},{"key":"1_CR24","doi-asserted-by":"publisher","unstructured":"Kapp\u00e9, T., Schmid, T., Silva, A.: A complete inference system for skip-free guarded Kleene algebra with tests. In: ESOP, pp. 309\u2013336 (2023). https:\/\/doi.org\/10.1007\/978-3-031-30044-8_12. https:\/\/arxiv.org\/abs\/2301.11301","DOI":"10.1007\/978-3-031-30044-8_12"},{"key":"1_CR25","unstructured":"Kapp\u00e9, T.: An elementary proof of the FMP for Kleene algebra (2024). https:\/\/arxiv.org\/abs\/2212.10931"},{"key":"1_CR26","unstructured":"Knuth, D.E.: The Art of Computer Programming, Volume I: Fundamental Algorithms, 3rd edn. Addison-Wesley, Boston (1997)"},{"issue":"2","key":"1_CR27","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. Comput. 110(2), 366\u2013390 (1994). https:\/\/doi.org\/10.1006\/inco.1994.1037","journal-title":"Inf. Comput."},{"key":"1_CR28","doi-asserted-by":"publisher","unstructured":"Kozen, D.: Kleene algebra with tests and commutativity conditions. In: TACAS, pp. 14\u201333 (1996). https:\/\/doi.org\/10.1007\/3-540-61042-1_35","DOI":"10.1007\/3-540-61042-1_35"},{"issue":"3","key":"1_CR29","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. ACM Trans. Program. Lang. Syst. 19(3), 427\u2013443 (1997). https:\/\/doi.org\/10.1145\/256167.256195","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"1_CR30","doi-asserted-by":"publisher","unstructured":"Kozen, D.: Myhill-Nerode relations on automatic systems and the completeness of Kleene algebra. In: STACS, pp. 27\u201338 (2001). https:\/\/doi.org\/10.1007\/3-540-44693-1_3","DOI":"10.1007\/3-540-44693-1_3"},{"key":"1_CR31","first-page":"117","volume":"24","author":"D Kozen","year":"2003","unstructured":"Kozen, D.: Automata on guarded strings and applications. Matematica Contemporanea 24, 117\u2013139 (2003)","journal-title":"Matematica Contemporanea"},{"key":"1_CR32","doi-asserted-by":"publisher","unstructured":"Kozen, D., Mamouras, K.: Kleene algebra with equations. In: ICALP, pp. 280\u2013292 (2014). https:\/\/doi.org\/10.1007\/978-3-662-43951-7_24","DOI":"10.1007\/978-3-662-43951-7_24"},{"key":"1_CR33","doi-asserted-by":"publisher","unstructured":"Kozen, D., Patron, M.C.: Certification of compiler optimizations using Kleene algebra with tests. In: CL, pp. 568\u2013582 (2000). https:\/\/doi.org\/10.1007\/3-540-44957-4_38","DOI":"10.1007\/3-540-44957-4_38"},{"key":"1_CR34","doi-asserted-by":"publisher","unstructured":"Kozen, D., Smith, F.: Kleene algebra with tests: completeness and decidability. In: CSL, pp. 244\u2013259 (1996). https:\/\/doi.org\/10.1007\/3-540-63172-0_43","DOI":"10.1007\/3-540-63172-0_43"},{"key":"1_CR35","doi-asserted-by":"publisher","unstructured":"Kozen, D., Tseng, W.D.: The B\u00f6hm-Jacopini theorem is false, propositionally. In: MPC, pp. 177\u2013192 (2008). https:\/\/doi.org\/10.1007\/978-3-540-70594-9_11","DOI":"10.1007\/978-3-540-70594-9_11"},{"key":"1_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/BFb0032022","volume-title":"Automata, Languages and Programming","author":"D KROB","year":"1990","unstructured":"KROB, D.: A complete system of B-rational identities. In: Paterson, M.S. (ed.) ICALP 1990. LNCS, vol. 443, pp. 60\u201373. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/BFb0032022"},{"key":"1_CR37","doi-asserted-by":"publisher","unstructured":"Kuznetsov, S.L.: On the complexity of reasoning in Kleene algebra with commutativity conditions. In: ICTAC, pp. 83\u201399 (2023). https:\/\/doi.org\/10.1007\/978-3-031-47963-2_7","DOI":"10.1007\/978-3-031-47963-2_7"},{"issue":"1","key":"1_CR38","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1109\/TEC.1960.5221603","volume":"9","author":"R McNaughton","year":"1960","unstructured":"McNaughton, R., Yamada, H.: Regular expressions and state graphs for automata. IRE Trans. Electron. Comput. 9(1), 39\u201347 (1960). https:\/\/doi.org\/10.1109\/TEC.1960.5221603","journal-title":"IRE Trans. Electron. Comput."},{"issue":"3","key":"1_CR39","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1016\/0022-0000(84)90023-0","volume":"28","author":"R Milner","year":"1984","unstructured":"Milner, R.: A complete inference system for a class of regular behaviours. J. Comput. Syst. Sci. 28(3), 439\u2013466 (1984). https:\/\/doi.org\/10.1016\/0022-0000(84)90023-0","journal-title":"J. Comput. Syst. Sci."},{"key":"1_CR40","doi-asserted-by":"publisher","unstructured":"Pous, D.: Symbolic algorithms for language equivalence and Kleene algebra with tests. In: POPL, pp. 357\u2013368 (2015). https:\/\/doi.org\/10.1145\/2676726.2677007","DOI":"10.1145\/2676726.2677007"},{"key":"1_CR41","doi-asserted-by":"publisher","unstructured":"Pous, D., Rot, J., Wagemaker, J.: On tools for completeness of Kleene algebra with hypotheses. Log. Methods Comput. Sci. 20(2) (2024). https:\/\/doi.org\/10.46298\/LMCS-20(2:8)2024","DOI":"10.46298\/LMCS-20(2:8)2024"},{"key":"1_CR42","doi-asserted-by":"publisher","unstructured":"Pous, D., Wagemaker, J.: Completeness theorems for Kleene algebra with tests and top. Log. Methods Comput. Sci. 20(3) (2024). https:\/\/doi.org\/10.46298\/LMCS-20(3:27)2024","DOI":"10.46298\/LMCS-20(3:27)2024"},{"key":"1_CR43","doi-asserted-by":"publisher","unstructured":"Rooduijn, J., Kozen, D., Silva, A.: A cyclic proof system for guarded Kleene algebra with tests. In: IJCAR, pp. 257\u2013275 (2024). https:\/\/doi.org\/10.1007\/978-3-031-63501-4_14","DOI":"10.1007\/978-3-031-63501-4_14"},{"key":"1_CR44","doi-asserted-by":"publisher","unstructured":"R\u00f3\u017cowski, W., Kapp\u00e9, T., Kozen, D., Schmid, T., Silva, A.: Probabilistic guarded KAT modulo bisimilarity: completeness and complexity. In: ICALP (2023). https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2023.136","DOI":"10.4230\/LIPIcs.ICALP.2023.136"},{"issue":"1","key":"1_CR45","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1145\/321312.321326","volume":"13","author":"A Salomaa","year":"1966","unstructured":"Salomaa, A.: Two complete axiom systems for the algebra of regular events. J. ACM 13(1), 158\u2013169 (1966). https:\/\/doi.org\/10.1145\/321312.321326","journal-title":"J. ACM"},{"key":"1_CR46","doi-asserted-by":"publisher","unstructured":"Schmid, T., Kapp\u00e9, T., Kozen, D., Silva, A.: Guarded Kleene algebra with tests: coequations, coinduction, and completeness. In: ICALP, pp. 142:1\u2013142:14 (2021). https:\/\/doi.org\/10.4230\/LIPICS.ICALP.2021.142","DOI":"10.4230\/LIPICS.ICALP.2021.142"},{"key":"1_CR47","doi-asserted-by":"publisher","unstructured":"Schmid, T., Rot, J., Silva, A.: On star expressions and coalgebraic completeness theorems. In: MFPS, pp. 242\u2013259 (2021). https:\/\/doi.org\/10.4204\/EPTCS.351.15","DOI":"10.4204\/EPTCS.351.15"},{"key":"1_CR48","unstructured":"Sedl\u00e1r, I.: Kleene algebra with dynamic tests: completeness and complexity (2023). https:\/\/arxiv.org\/abs\/2311.06937"},{"key":"1_CR49","doi-asserted-by":"publisher","unstructured":"Smolka, S., Foster, N., Hsu, J., Kapp\u00e9, T., Kozen, D., Silva, A.: Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time. In: POPL, pp. 61:1\u201361:28 (2020). https:\/\/doi.org\/10.1145\/3371129","DOI":"10.1145\/3371129"},{"issue":"2","key":"1_CR50","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1145\/321879.321884","volume":"22","author":"RE Tarjan","year":"1975","unstructured":"Tarjan, R.E.: Efficiency of a good but not linear set union algorithm. J. ACM 22(2), 215\u2013225 (1975). https:\/\/doi.org\/10.1145\/321879.321884","journal-title":"J. ACM"},{"issue":"6","key":"1_CR51","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. Commun. ACM 11(6), 419\u2013422 (1968). https:\/\/doi.org\/10.1145\/363347.363387","journal-title":"Commun. ACM"},{"key":"1_CR52","unstructured":"Van Koevering, S., Rozowski, W., Silva, A.: Weighted GKAT: completeness and complexity (2025). https:\/\/arxiv.org\/abs\/2504.20385"},{"key":"1_CR53","unstructured":"Watson, B.W.: A taxonomy of finite automata construction algorithms. Technical report, Technische Universiteit Eindhoven (1993). https:\/\/research.tue.nl\/files\/2482472\/9313452"},{"key":"1_CR54","doi-asserted-by":"publisher","unstructured":"Zhang, C., Kapp\u00e9, T., Narv\u00e1ez, D.E., Naus, N.: CF-GKAT: efficient validation of control-flow transformations. In: POPL, pp. 21:1\u201321:27 (2025). https:\/\/doi.org\/10.1145\/3704857","DOI":"10.1145\/3704857"}],"container-title":["Lecture Notes in Computer Science","Logic, Language, Information, and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-99536-1_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,7]],"date-time":"2025-12-07T14:07:12Z","timestamp":1765116432000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-99536-1_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,1]]},"ISBN":["9783031995354","9783031995361"],"references-count":54,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-99536-1_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025,8,1]]},"assertion":[{"value":"1 August 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"WoLLIC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Workshop on Logic, Language, Information, and Computation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Porto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"wollic2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/wollic.org\/wollic2025","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}