Verified decision procedures for MSO on words based on derivatives of regular expressions.

Dmitriy Traytel, Tobias Nipkow

Browse the full ICFP paper archive.