Dmitriy Traytel, Tobias Nipkow. Verified decision procedures for MSO on words based on derivatives of regular expressions. In Greg Morrisett, Tarmo Uustalu, editors, ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25 - 27, 2013. pages 3-12, ACM, 2013. [doi]
Abstract is missing.