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.
|Title of host publication||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|
|Place of Publication||Berlin|
|Number of pages||24|
|Publication status||Published - 2001|
|Name||Lecture Notes in Comput. Sci.|
Plotkin, G., & Power, J. (2001). Adequacy for algebraic effects. In 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 (Vol. 2030, pp. 1-24). (Lecture Notes in Comput. Sci.). Berlin: Springer. https://doi.org/10.1007/3-540-45315-6_1