Adequacy for algebraic effects

Gordon Plotkin, John Power

Research output: Chapter in Book/Report/Conference proceedingChapter

74 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 Dive into the research topics of 'Adequacy for algebraic effects'. Together they form a unique fingerprint.

Cite this