The study of programming language semantics lets us fix the meaning of language concepts and helps us understand how programs behave and interact with their environment. Domain theory has first been developed to give a semantics to recursion in programming languages, but it also serves as a great theory to model various algebraic effects such as non-determinism, partial functions, side effects and numerous other forms of computation.
In this work, we present a general framework to construct algebraic effects in domain theory. We first describe a method to represent various algebraic effects, and then interpret these effects using initial algebra semantics. We show that several well-known examples of algebraic effects fit our framework.
Our work makes use of various features of Homotopy Type Theory and is formalized in Cubical Agda.