WG211/M23Gordon

Many libraries and abstractions have constraints on the order in which programs perform certain operations. Sequential (flow-sensitive) effect systems are one powerful approach to checking that these constraints are followed, but currently the limits on what sorts of protocols can be checked this way are unknown. We resolve this by exploring the synthesis of sequential effect systems from a broad class of automata known as valence automata, which abstract an automataton's storage mechanism by a monoid of storage updates. This unified model of storage mechanisms offers a way to generate an algebraic characterization of an effect system from automata up to and including Turing Machines. The unified storage abstraction then reduces questions of decidability for individual effect systems to problems involving rational subsets of the storage monoids. Come for the effect systems, stay for the theory of computation and computer algebra!