BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A Formalisation of the Myhill-Nerode Theorem based on Regular Expr
 essions - Christian Urban (University of Cambridge)
DTSTART:20101109T130000Z
DTEND:20101109T140000Z
UID:TALK26948@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:There are countless textbooks on regular languages. Nearly 100
 % of them introduce the subject by describing finite automata and only men
 tioning on the side a connection with regular expressions. Unfortunately\,
  automata are a hassle for formalisations in existing \ntheorem provers. T
 he reason is that automata need to be represented as graphs or matrices\, 
 neither of which can be easily defined as algebraic datatype. In contrast\
 , regular expressions can be defined easily as datatype and a correspondin
 g reasoning infrastructure comes for free. We show in this talk that a cen
 tral result from formal \nlanguage theory\, the Myhill-Nerode theorem\, ca
 n be recreated using only regular expressions. This will involve ideas fro
 m term rewriting and unification theory. The Myhill-Nerode theorem provide
 s necessary and sufficient conditions for a language to be regular.\n\nThi
 s is joint work with Chunhan Wu and Xingyuan Zhang. The work was partly in
 spired by a nice paper of Scott Owens on regular expression matching. \n
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR