DocumentCode
2597038
Title
Computational lambda-calculus and monads
Author
Moggi, Eugenio
Author_Institution
Lab. for Found. of Comput. Sci., Edinburgh Univ., UK
fYear
1989
fDate
5-8 Jun 1989
Firstpage
14
Lastpage
23
Abstract
The λ-calculus is considered a useful mathematical tool in the study of programming languages. However, if one uses βη-conversion to prove equivalence of programs, then a gross simplification is introduced. The author gives a calculus based on a categorical semantics for computations, which provides a correct basis for proving equivalence of programs, independent from any specific computational model
Keywords
formal languages; formal logic; βη-conversion; λ-calculus; categorical semantics; computational lambda-calculus; equivalence of programs; mathematical tool; monads; programming languages; prove; Calculus; Computer languages; Computer science; Contracts; Logic programming; Mathematical model; Mathematical programming; Reasoning about programs;
fLanguage
English
Publisher
ieee
Conference_Titel
Logic in Computer Science, 1989. LICS '89, Proceedings., Fourth Annual Symposium on
Conference_Location
Pacific Grove, CA
Print_ISBN
0-8186-1954-6
Type
conf
DOI
10.1109/LICS.1989.39155
Filename
39155
Link To Document