Research

Adequacy for algebraic effects


Reference:

Plotkin, G. and Power, J., 2001. Adequacy for algebraic effects. 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.

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.

Details

Item Type Conference or Workshop Items (UNSPECIFIED)
CreatorsPlotkin, G.and Power, J.
DOI10.1007/3-540-45315-6_1
DepartmentsFaculty of Science > Computer Science
StatusPublished
ID Code5613
Additional InformationGenova, 2001

Export

Actions (login required)

View Item