Notions of computation and monads Export

@article{citeulike:456366, 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.}, address = {Duluth, MN, USA}, author = {Moggi, Eugenio}, citeulike-article-id = {456366}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=116984}, citeulike-linkout-1 = {http://dx.doi.org/10.1016/0890-5401(91)90052-4}, citeulike-linkout-2 = {http://www.disi.unige.it/person/MoggiE/ftp/ic91.pdf}, doi = {10.1016/0890-5401(91)90052-4}, issn = {0890-5401}, journal = {Information and Computation}, keywords = {category-theory, equivalence, lambda-calculus, monads, semantics}, month = {July}, number = {1}, pages = {55--92}, posted-at = {2009-02-17 11:00:58}, priority = {2}, publisher = {Academic Press, Inc.}, title = {Notions of computation and monads}, url = {http://dx.doi.org/10.1016/0890-5401(91)90052-4}, volume = {93}, year = {1991} }

TY - JOUR ID - citeulike:456366 L3 - citeulike-article-id:456366 N2 - 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. IS - 1 JF - Information and Computation SN - 0890-5401 AD - Duluth, MN, USA EP - 92 TI - Notions of computation and monads PB - Academic Press, Inc. VL - 93 SP - 55 KW - category-theory KW - equivalence KW - lambda-calculus KW - monads KW - semantics AU - Moggi, Eugenio PY - 1991/07// UR - http://dx.doi.org/10.1016/0890-5401(91)90052-4 ER -