Adequacy for algebraic effects

Gordon Plotkin, John Power

Research output: Chapter in Book/Report/Conference proceedingChapter

67 Citations (Scopus)

Abstract

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.
Original languageEnglish
Title of host publicationFoundations 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 PublicationBerlin
PublisherSpringer
Pages1-24
Number of pages24
Volume2030
DOIs
Publication statusPublished - 2001

Publication series

NameLecture Notes in Comput. Sci.
PublisherSpringer

    Fingerprint

Cite this

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