Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny

Stefan Zetzsche, Wojciech Rozowski

Regular expressions are commonly understood in terms of their denotational semantics, that is, through formal languages -- the regular languages. This view is inductive in nature:…