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

DOI10.1145/2500365.2500612zbMath1323.68346OpenAlexW2166971839MaRDI QIDQ5244782

Dmitriy Traytel, Tobias Nipkow

Publication date: 30 March 2015

Published in: Proceedings of the 18th ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/20.500.11850/106053

zbMATH Keywords

regular expressionsdecision procedureinteractive theorem provingIsabelleWS1SMSOBrzozowski derivatives

Mathematics Subject Classification ID

Related Items (3)

Verified decision procedures for MSO on words based on derivatives of regular expressions ⋮ Two-Way Automata in Coq ⋮ Derivatives for Enhanced Regular Expressions

Uses Software

• Isabelle
• MSO_Regex_Equivalence

This page was built for publication: Verified decision procedures for MSO on words based on derivatives of regular expressions