[Club2] Wed. Nov 24, 14:00: Tobias Nipkow

[Alexander Krauss]

Dear all,

Tomorrow, we will have more automata-free language theory. Tobias will 
speak about our proof pearl on deciding regular expression equivalence.


Regular Expression Equivalence and Relation Algebra
====================================================
Wed. Nov 24, 14:00, MI 00.09.055 ("Alan Turing")

We describe and verify an elegant equivalence checker for regular
expressions. It works by constructing a bisimulation relation between
(derivatives of) regular expressions.  By mapping regular expressions to
binary relations, an automatic and complete proof method for (in)equalities
of binary relations over union, composition and (reflexive) transitive
closure is obtained.