Computational lambda-calculus and monads. (English) Zbl 0716.03007

Moggi, Eugenio

Logic in computer science, Proc. 4th Annual Symp., Pacific Grove/CA (USA) 1989, 14-23 (1989).

Summary: [For the entire collection see Zbl 0713.00018.]
\(\lambda\)-calculus is considered a useful mathematical tool in the study of programming languages. However, if one uses \(\beta\eta\)-conversion to prove equivalence of programs, then a considerable simplification is introduced. We give a calculus based on a categorical semantics for computations, which provides a correct basis for proving equivalence of programs, independent of any specific computational model.

MSC:

03B40	Combinatory logic and lambda calculus
03B70	Logic in computer science
68Q55	Semantics in the theory of computing

Keywords:

\(\lambda \) -calculus; categorical semantics for computations; equivalence of programs