A regular expression toolkit
Supervisor
Suitable for
Abstract
Various constructions on regular expressions and finite automata are nice to contemplate, but hard to describe informally
without sinking in a mire of nested subscripts, and hard to implement in a conventional way without becoming lost in a maze
of twisty little pointers, all alike. The goal in this project is to come up with a perspicuous implementation of some of
these algorithms in a suitable programming language such as Haskell or OCaml, abstracting shared patterns such as fixpoint
computations as higher-order functions. A suitable target would be a program for marking Models of Computation homework: it
would accept two regular expressions on the command line, and either verify that they were equivalent or print a word that
matched one expression but not the other. More ambitious would be a program that could also prove the equivalence from the
Kozen axioms.