Adequacy for Infinitary Algebraic Effects (Abstract)

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Moggi famously proposed a monadic account of computational effects [Mog89, Mog91, BHM02]; this account includes the computational λ-calculus, a core call-by-value functional programming language. Moggi endowed the computational λ-calculus with an effect-oriented denotational semantics by taking the denotations of terms to be morphisms in the Kleisli category of the monad. The question naturally then arises as to whether one can give a correspondingly general treatment of operational semantics.
In the algebraic theory of effects [PP02, PP04, HPP06], a refinement of Moggi’s theory, the effects are obtained by appropriate operations, and Moggi’s monad is then generated by an equational theory over these operations. In a previous paper with John Power [PP01] we gave a general adequacy theorem for the computational λ-calculus for the case of monads generated by finitary operations. This covers examples such as (probabilistic) nondeterminism and exceptions. The main idea is to evaluate terms symbolically in the absolutely free algebra with the same signature as the equational theory. Without recursion, the evaluated terms are finite; with recursion, they may be infinitely deep.
Original languageEnglish
Title of host publicationAlgebra and Coalgebra in Computer Science
Subtitle of host publicationThird International Conference, CALCO 2009, Udine, Italy, September 7-10, 2009. Proceedings
PublisherSpringer Berlin Heidelberg
Number of pages2
ISBN (Electronic)978-3-642-03741-2
ISBN (Print)978-3-642-03740-5
Publication statusPublished - 2009

Fingerprint Dive into the research topics of 'Adequacy for Infinitary Algebraic Effects (Abstract)'. Together they form a unique fingerprint.

Cite this