Title :
Computational lambda-calculus and monads
Author_Institution :
Lab. for Found. of Comput. Sci., Edinburgh Univ., UK
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;
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
DOI :
10.1109/LICS.1989.39155
