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

Introduction Regular expressions are one of the most ubiquitous formalisms of theoretical computer science. Commonly, they are understood in terms of their denotational semantics, that is, through formal languages — the regular languages. This view is inductive in nature: two primitives ar...