On the relations between monadic semantics

We present a simple computational metalanguage with general recursive types and multiple notions of effects, through which a variety of concrete denotational semantics can be conveniently factored, by suitably interpreting the effects as monads. We then propose a methodology for relating two such interpretations of the metalanguage, with the aim of showing that the semantics they induce agree for complete programs. As a prototypical instance of such a relation, we use the framework to show agreement between a direct and a continuation semantics of the simple, untyped functional language from Reynolds’s original paper on the subject.