## Computational Lambda-Calculus and Monads

**E. Moggi**
*Abstract:* The lambda-calculus is considered an useful
mathematical tool in the study of programming languages, since
programs can be *identified* with lambda-terms. However, if
one goes further and uses beta eta -conversion to prove equivalence
of programs, then a gross simplification is introduced, that may
jeopardise the applicability of theoretical results to real
situations. In this paper we introduce a new calculus based on
categorical semantics for *computations*. This calculus
provides a correct basis for proving equivalence of programs,
independent from any specific computational model.

*LFCS report ECS-LFCS-88-66*

A revised version
appeared in the Proceedings of the Fourth Annual Symposium on Logic
in Computer Science (LICS), Pacific Grove, California, June 5th-8th
1989, pp14-23.

Previous |

Index |

Next