Notions of computation and monads

The work

AuthorsEugenio Moggi
Typearticle
Year1991
Citekeymoggi1991notions

Where it appeared

Published inInformation and Computation
PublisherElsevier
Volume93
Issue1
Pages55--92

Identifiers

DOI10.1016/0890-5401(91)90052-4

Abstract

The λ-calculus is considered an useful mathematical tool in the study of programming languages, since programs can be identified with λ-terms. However, if one goes further and uses βη-conversion to prove equivalence of programs, then a gross simplification is introduced (programs are identified with total functions from values to values), that may jeopardise the applicability of theoretical results. In this paper we introduce calculi based on a categorical semantics for computations, that provide a correct basis for proving equivalence of programs, for a wide range of notions of computation.

A copy is held

pdf, 269.4 kB. Not published — it may be under copyright. The facts and links here are.

How it got here

How it got hereimport via bibtex
Added2026-08-09 00:00 UTC
Approved bya person 2026-08-16 15:29 UTC

Filed under

the-copy-is-not-the-work what-a-program-means

Cite it as

@article{moggi1991notions,
  title        = {Notions of computation and monads},
  author       = {Eugenio Moggi},
  year         = {1991},
  journal      = {Information and Computation},
  volume       = {93},
  number       = {1},
  pages        = {55--92},
  publisher    = {Elsevier},
  doi          = {10.1016/0890-5401(91)90052-4},
}

This record lives at https://refs.drheap.org/moggi1991notions/ and will keep doing so.