mmmodularity!

» by Scott Kilpatrick

Henglein and Nielsen. Regular expression containment: coinductive axiomatization and computational interpretation, POPL 2011. (ACM)

* * *

Primarily, I like this paper as further elucidation of the propositions-as-types principle. They didn’t originate the idea of regexps as types, but they did connect terms of those types to the parse trees (i.e. proofs) that form various strings in a regexp. They exploit that proof-term connection to show, for example, that by writing a simple functional program you can prove that one regular expression is contained in (or equal to) another.

In the final section they explain how their insights can be used to generate efficient bit codings of strings that match a given regexp. Their results seem to indicate a more efficient (than ASCII) representation technique when storing strings of certain forms. Finally, the last “application-level” idea involves a reinterpretation of the A* regexp from a “cons list” type to a fixed-point recursive type, which allows them to recover the usual, optimal 8-bit encoding of general ASCII strings. Neat!

One more thing: they use a “semantic predicate” on derivations (i.e. proof terms) — as opposed to a predicate on pieces of syntax — in one of the inference rules for their system. I haven’t seen that technique before. I dig it.