Regular Sets
Regular Sets and Expressions. This is a library of constructions on regular expressions and languages. It provides the operations of concatenation, Kleene star and derivative on languages. Regular expressions and their meaning are defined. An executable equivalence checker for regular expressions is verified; it does not need automata but works directly on regular expressions. By mapping regular expressions to binary relations, an automatic and complete proof method for (in)equalities of binary relations over union, concatenation and (reflexive) transitive closure is obtained. Extended regular expressions with complement and intersection are also defined and an equivalence checker is provided.
Keywords for this software
References in zbMATH (referenced in 14 articles )
Showing results 1 to 14 of 14.
Sorted by year (- Doczkal, Christian; Smolka, Gert: Regular language representations in the constructive type theory of Coq (2018)
- Armstrong, Alasdair; Gomes, Victor B. F.; Struth, Georg: Building program construction and verification tools from algebraic principles (2016)
- Ausaf, Fahad; Dyckhoff, Roy; Urban, Christian: POSIX lexing with derivatives of regular expressions (proof pearl) (2016)
- Rot, Jurriaan; Bonsangue, Marcello; Rutten, Jan: Proving language inclusion and equivalence by coinduction (2016)
- Moreira, Nelma; Pereira, David; Melo de Sousa, Simão: Deciding Kleene algebra terms equivalence in Coq (2015)
- Traytel, Dmitriy; Nipkow, Tobias: Verified decision procedures for MSO on words based on derivatives of regular expressions (2015)
- Armstrong, Alasdair; Struth, Georg; Weber, Tjark: Programming and automating mathematics in the Tarski-Kleene hierarchy (2014)
- Wu, Chunhan; Zhang, Xingyuan; Urban, Christian: A formalisation of the Myhill-Nerode theorem based on regular expressions (2014)
- Armstrong, Alasdair; Struth, Georg: Automated reasoning in higher-order regular algebra (2012)
- Braibant, Thomas; Pous, Damien: Deciding Kleene algebras in \textttCoq (2012)
- Krauss, Alexander; Nipkow, Tobias: Proof Pearl: regular expression equivalence and relation algebra (2012)
- Laurence, Michael R.; Struth, Georg: On completeness of omega-regular algebras (2012)
- Moreira, Nelma; Pereira, David; Melo de Sousa, Simão: Deciding regular expressions (in-)equivalence in Coq (2012)
- Coquand, Thierry; Siles, Vincent: A decision procedure for regular expression equivalence in type theory (2011)