• People
• Events
• Research

Computational Lambda-Calculus and Monads

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.