EVENT

ERATO Project Colloquium by Agnishom Chattopadhyay

On Tuesday 3 December, Agnishom Chattopadhyay (National Institute of Informatics) will give a talk, "Verified Regular Expression Matching - Derivatives, NFAs and more", for our project colloquium at 16:30. Further details can be found below.

Title:

Verified Regular Expression Matching - Derivatives, NFAs and more

Speaker:

Agnishom Chattopadhyay (National Institute of Informatics)

Abstract:

Regular Expressions are a foundational element of the theory and practice of formal methods. In this talk, we will discuss three avenues towards the formalization of regular expression matching in a proof assistant (namely, Coq). Derivatives have been popular in the discourse recently - their semantics are elegant, and their mechanics can be described easily in a functional language. However, tactfully managing the sizes of derivatives can be a challenge. The direct simulation of Thompson NFAs is efficient, but doing so in a purely functional manner can be challenging. The technique of Marked Regular Expressions is lesser known - they can be implemented in a purely functional manner, and this algorithm would have the same asymptotic complexity as the simulation of NFAs.

Time/Date:

16:30- / Tuesday 3 December , 2024

Place:

NII Room 1310A and Online

Link:

For the latest information about ERATO colloquium/seminar, please see the webpage.
https://docs.google.com/document/d/1Qrg4c8XDkbO3tmns6tQwxn5lGHOrBON5LtHXXTpXDeA/edit

Contact:

Kittiphon Phalakarn (ERATO MMSD Colloquium Organizer)
Email: kphalakarn[at] nii.ac.jp