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.
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.
Previous | Index | Next An error occured whilst processing this directive