Email Gateway (Aug 18 2022 at 15:21): Email Gateway (Aug 18 2022 at 15:21):From: Tobias Nipkow <nipkow@in.tum.de>
A new entry has recently made it into the development branch of the AFP:
Regular Sets and Expressions
Alexander Krauss and Tobias Nipkow
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.
http://afp.sourceforge.net/devel-entries/Regular-Sets.shtml
Last updated: Apr 25 2024 at 01:08 UTC