[Club2] Reminder for talk on Wednesday

[Christian Urban]

Dear All,

Just a reminder for my talk tomorrow at 
14:00 in room Alan Turing. The topic will be 
regular expressions (something non-nominal ;o)

Best wishes,
Christian




>
> A Formalisation of the Myhill-Nerode Theorem based
> on Regular Expressions
>
> There are countless textbooks on regular languages. Nearly 100% 
> of them introduce the subject by describing finite automata and 
> only mentioning on the side a connection with regular expressions. 
> Unfortunately, automata are a hassle for formalisations. The 
> reason is that in full generality they need to be represented as 
> graphs or matrices, neither of which can be easily defined as 
> datatype. In contrast, regular expressions can be defined easily 
> as datatype and a corresponding reasoning infrastructure comes for 
> free. We show in this talk that a central result from formal 
> language theory - the Myhill-Nerode theorem - can be recreated 
> using only regular expressions. This will involve ideas from term 
> rewriting and unification theory. The Myhill-Nerode theorem provides 
> necessary and sufficient conditions for a language to be regular.
>
>
> This is joint work with Chunhan Wu and Xingyuan Zhang
> (who I visited over the summer in Nanjing). The work was 
> partly inspired by two nice functional pearls by Harper
> and by Yi.