Defined algebraic operations

Defined algebraic operations ("DAO") is a novel model of programming, which sits broadly between imperative and purely functional programming. DAO expresses many control-flow idioms in a fashion similar to algebraic effect handling. But operation definition is lexical, and commutes with sequencing (when that type-checks). DAO has three particular strengths. Firstly, DAO automatically avoids name clashes when writing higher-order programs with nonlocal control. This is demonstrated with a simple example. Secondly, certain buggy programs do not type check due to the lexical nature of DAO. Thirdly, it validates a strong "theory-dependent" logic, which uses properties of operation definitions to add equivalences inside their scope. For instance, under an operation definition for state, most state equations hold, even under lambdas --- the analogous statement for handling is false. This lends extra credibility to the claim that DAO is a form of user-defined effects. To substantiate these claims, we give a concrete DAO language and logic based on the fine-grain call-by-value lambda calculus, and a number of examples. As an additional contribution, we give a simpler presentation of a method for proving coherence of denotational semantics, first presented in a more sophisticated setting by Biernacki and Polesiuk