COPLAS talk: Proof-directed program transformation: A functional account of efficient regular expression matching

On 20 August, Andrzej Filinski, associate professor at DIKU, will give a COPLAS talk.

Abstract

We show how to systematically derive an efficient regular-expression (regex) matcher using a variety of program-transformation techniques, but very little specialized formal-language and automata theory.

Starting from the standard specification of the set-theoretic semantics of regular expressions, we proceed via a continuation-based backtracking matcher, to a classical, table driven state machine. 

All steps of the development are supported by self-contained (and machine-verified) equational correctness proofs.

Program

11:05-11:25 Video presentation of talk (to be presented at ICFP 2021)
11:25-12:00 Live discussion

Bio

Andrzej Filinski is DIKU faculty. Amongst other things he has contributed pioneering research to continuation-style passing, monads and their semantics.

Join the talk

All are welcome. No registration required.  Feel free to forward this invitation. 

More information

To be informed about COPLAS and related talks, visit https://list.ku.dk/postorius/lists/sci-diku-prog-lang.list.ku.dk.