BEGIN:VCALENDAR
PRODID:-//eluceo/ical//2.0/EN
VERSION:2.0
CALSCALE:GREGORIAN
BEGIN:VEVENT
UID:www.tcs.tifr.res.in/event/173
DTSTAMP:20230914T125913Z
SUMMARY:Building Certificates of Regular Expressions Equivalence
DESCRIPTION:Speaker: Benoit Razet\nTata Institute of Fundamental Research\n
 School of Technology and Computer Science\nHomi Bhabha Road\n\nAbstract: \
 nRegular expressions are mostly known as pattern matching expressions in s
 cripting languages (Perl\, sed\, awk\, etc.). They are also theoretically 
 studied for their strong relationship with Automata Theory. A regular expr
 ession denote a language (set of words) and two regular expressions are eq
 uivalent when they denote the same language. The equivalence problem is de
 cidable and furthermore\, any equivalence can be proved axiomatically. Var
 ious such axiomatisations have flourished during the last fifty years\, we
  will survey the most important ones.\n\nEvery axiomatisation come togethe
 r with a proof of completeness of the following form: if two regular expre
 ssions are equivalent then there exists  proof within the axiomatic system
 . In principle\, when this completeness proof is constructive one can extr
 act from it an algorithm that produces a certificate of the equivalence. W
 e have filled the gap developping a program (written in OCaml) that comput
 es certificates. For this purpose we have designed a domain specific proof
  system with a language of commands for composing a certificate checkable 
 within this system (this is a joint work with Bodhayan Roy).\n
URL:https://www.tcs.tifr.res.in/web/events/173
DTSTART;VALUE=DATE:20110316
LOCATION:A-212 (STCS Seminar Room)
END:VEVENT
END:VCALENDAR