On the relations between monadic semantics

TY - JOUR

T1 - On the relations between monadic semantics

AU - Filinski, Andrzej

PY - 2007

Y1 - 2007

N2 - 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.

AB - 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.

U2 - 10.1016/j.tcs.2006.12.027

DO - 10.1016/j.tcs.2006.12.027

M3 - Journal article

SN - 0304-3975

VL - 375

SP - 41

EP - 75

JO - Theoretical Computer Science

JF - Theoretical Computer Science

IS - 1-3

ER -