@article(aboul-hosn06:_kat_ml, author = "Kamal Aboul-Hosn and Dexter Kozen", year = "2006", title = "{KAT-ML}: An Interactive Theorem Prover for {K}leene Algebra with Tests", journal = "Journal of Applied Non-Classical Logics", volume = "16", number = "1--2", pages = "9--33", doi = "10.3166/jancl.16.9-33", ) @phdthesis(almeida11:_equiv_of_regul_languag, author = "Marco Almeida", year = "2011", title = "Equivalence of regular languages: an algorithmic approach and complexity analysis", school = "Faculdade de Ci\^{e}ncias das Universidade do Porto", note = "\url {http://www.dcc.fc.up.pt/~mfa/thesis.pdf}", ) @article(almeida09:_antim_mosses, author = "Marco Almeida and Nelma Moreira and Rog\IeC {\'e}rio Reis", year = "2009", title = "{Antimirov} and {Mosses}'s rewrite system revisited", journal = "International Journal of Foundations of Computer Science", volume = "20", number = "04", pages = "669 -- 684", doi = "10.1142/S0129054109006802", ) @article(antimirov96:_partial_deriv_regul_expres_finit_autom_const, author = "Valentin M. Antimirov", year = "1996", title = "Partial Derivatives of Regular Expressions and Finite Automaton Constructions.", journal = "Theoret. Comput. Sci.", volume = "155", number = "2", pages = "291--319", doi = "10.1016/0304-3975(95)00182-4", ) @inproceedings(antimirov94:_rewrit_exten_regul_expres, author = "Valentin M. Antimirov and Peter D. Mosses", year = "1994", title = "Rewriting Extended Regular Expressions", editor = "G. Rozenberg and A. Salomaa", booktitle = "Developments in Language Theory", publisher = "World Scientific", pages = "195 -- 209", ) @incollection(babu11:_chop_expres_and_discr_durat_calcul, author = "S. Ajesh Babu and Paritosh K Pandya", year = "2011", title = "Chop Expressions and Discrete Duration Calculus", booktitle = "Modern Applications of Automata Theory", volume = "2", publisher = "World Scientific", pages = "1--30", ) @article(chen04:_coalg_approac_to_kleen_algeb_with_tests, author = "H. Chen and R. Pucella", year = "2004", title = "A coalgebraic approach to {Kleene} algebra with tests", journal = "Theor. Comp. Sci.", volume = "327", number = "1-2", pages = "23--44", doi = "10.1016/j.tcs.2004.07.020", ) @techreport(cohen96:_compl_of_kleen_algeb_with_tests, author = "Ernie Cohen and Dexter Kozen and Frederick Smith", year = "1996", title = "The complexity of {K}leene algebra with tests", type = "Technical Report", number = "TR96-1598", institution = "Computer Science Department, Cornell University", ) @misc(fado_online, author = "Project FAdo", year = "{Access date:1.1.2012}", title = "{FAdo}: tools for formal languages manipulation", howpublished = "\url {http://fado.dcc.fc.up.pt}", ) @article(frade11:_verif_condit_for_sourc_level_imper_progr, author = "Maria Jo{\~a}o Frade and Jorge Sousa Pinto", year = "2011", title = "Verification conditions for source-level imperative programs", journal = "Computer Science Review", volume = "5", number = "3", pages = "252--277", doi = "10.1016/j.cosrev.2011.02.002", ) @article(hoare69:_axiom_basis_for_comput_progr, author = "C. A. R. Hoare", year = "1969", title = "An axiomatic basis for computer programming", journal = "Comm. of the {ACM}", volume = "12", number = "10", pages = "576--580", doi = "10.1145/357980.358001", ) @inproceedings(hofner07:_autom_reason_in_kleen_algeb, author = "Peter H\'ofner and Georg Struth", year = "2007", title = "Automated Reasoning in {Kleene} Algebra", editor = "F. Pfenning", booktitle = "CADE 2007", series = "LNAI", volume = "4603", publisher = "Springer-Verlag", pages = "279--294", doi = "10.1007/978-3-540-73595-3-19", ) @article(kozen94:_compl_theor_for_kleen_algeb, author = "Dexter Kozen", year = "1994", title = "A completeness theorem for {K}leene algebras and the algebra of regular events", journal = "Infor. and Comput.", volume = "110", number = "2", pages = "366--390", doi = "10.1006/inco.1994.1037", ) @article(kozen97:_kleen_algeb_with_tests, author = "Dexter Kozen", year = "1997", title = "Kleene algebra with tests", journal = "Trans. on Prog. Lang. and Systems", volume = "19", number = "3", pages = "427--443", doi = "10.1145/256167.256195", ) @article(kozen00:_hoare_logic_and_kleen_algeb_with_tests, author = "Dexter Kozen", year = "2000", title = "On {H}oare logic and {K}leene algebra with tests", journal = "Trans. Comput. Logic", volume = "1", number = "1", pages = "60--76", doi = "10.1145/343369.343378", ) @article(kozen03:_autom_guard_strin_and_applic, author = "Dexter Kozen", year = "2003", title = "Automata on Guarded Strings and Applications", journal = "Mat{\'e}matica Contempor{\^a}nea", volume = "24", pages = "117--139", ) @techreport(kozen08:_coalg_theor_of_kleen_algeb_with_tests, author = "Dexter Kozen", year = "2008", title = "On the coalgebraic theory of {Kleene} algebra with tests", type = "Computing and Information Science Technical Reports", number = "{\url {http://hdl.handle.net/1813/10173}}", institution = "Cornell University", ) @inproceedings(kozen96:_kleen_algeb_with_tests, author = "Dexter Kozen and Frederick Smith", year = "1996", title = "Kleene algebra with tests: Completeness and decidability", editor = "D. van Dalen and M. Bezem", booktitle = "Proc. 10th CSL", series = "LNCS", volume = "1258", publisher = "Springer-Verlag", pages = "244--259", doi = "10.1007/3-540-63172-0-43", ) @article(mirkin66, author = "Boris Mirkin", year = "1966", title = "An Algorithm for Constructing a Base in a Language of Regular Expressions", journal = "Engineering Cybernetics", volume = "5", pages = "110--116", ) @inproceedings(rutten98:_autom_and_coind_exerc_in_coalg, author = "Jan J. M. M. Rutten", year = "1998", title = "Automata and Coinduction (An Exercise in Coalgebra)", editor = "Davide Sangiorgi and Robert de Simone", booktitle = "CONCUR'98 Concurrency Theory", series = "LNCS", volume = "1466", publisher = "Springer", pages = "194--218", doi = "10.1007/BFb0055624", ) @misc(team12:_ocaml, author = "The Caml team", year = "Access date: 1.5.2012", title = "Ocaml", howpublished = "\url {http://caml.inria.fr/ocaml/}", )