TY - CHAP

T1 - Adequacy for algebraic effects

AU - Plotkin, Gordon

AU - Power, John

N1 - Genova, 2001

PY - 2001

Y1 - 2001

N2 - Moggi proposed a monadic account of computational effects. He also presented the computational λ-calculus, λ c , a core call-by-value functional programming language for effects; the effects are obtained by adding appropriate operations. The question arises as to whether one can give a corresponding treatment of operational semantics. We do this in the case of algebraic effects where the operations are given by a single-sorted algebraic signature, and their semantics is supported by the monad, in a certain sense. We consider call-by-value PCF with— and without—recursion, an extension of λ c with arithmetic. We prove general adequacy theorems, and illustrate these with two examples: non-determinism and probabilistic nondeterminism.

AB - Moggi proposed a monadic account of computational effects. He also presented the computational λ-calculus, λ c , a core call-by-value functional programming language for effects; the effects are obtained by adding appropriate operations. The question arises as to whether one can give a corresponding treatment of operational semantics. We do this in the case of algebraic effects where the operations are given by a single-sorted algebraic signature, and their semantics is supported by the monad, in a certain sense. We consider call-by-value PCF with— and without—recursion, an extension of λ c with arithmetic. We prove general adequacy theorems, and illustrate these with two examples: non-determinism and probabilistic nondeterminism.

UR - http://dx.doi.org/10.1007/3-540-45315-6_1

U2 - 10.1007/3-540-45315-6_1

DO - 10.1007/3-540-45315-6_1

M3 - Chapter

VL - 2030

T3 - Lecture Notes in Comput. Sci.

SP - 1

EP - 24

BT - Foundations of Software Science and Computation Structures 4th International Conference, FOSSACS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2–6, 2001 Proceedings

PB - Springer

CY - Berlin

ER -