@article{moggi-1991-notions,
title = {Notions of computation and monads},
journal = {Information and Computation},
volume = {93},
number = {1},
pages = {55-92},
year = {1991},
note = {Selections from 1989 IEEE Symposium on Logic in Computer Science},
issn = {0890-5401},
doi = {https://doi.org/10.1016/0890-5401(91)90052-4},
url = {https://www.sciencedirect.com/science/article/pii/0890540191900524},
author = {Moggi, Eugenio},
abstract = {The λ-calculus is considered a 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.}
}