Computational lambda-calculus and monads. (English) Zbl 0716.03007
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.
\(\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 |