Adequacy for algebraic effects


Plotkin, G. and 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. Berlin: Springer, pp. 1-24. (Lecture Notes in Comput. Sci.)

Related documents:

This repository does not currently have the full-text of this item.
You may be able to access a copy if URLs are provided below.

Official URL:


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.


Item Type Book Sections
CreatorsPlotkin, G.and Power, J.
DepartmentsFaculty of Science > Computer Science
ID Code5613
Additional InformationGenova, 2001


Actions (login required)

View Item