Denis Firsov, Tarmo Uustalu: Certified Parsing of Regular Languages. CPP 2013: 98-113