Computational lambda-calculus and monads
Top Cited Papers
- 7 January 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
The 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 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
This publication has 5 references indexed in Scilit:
- The theory of constructions: categorical semantics and topos-theoretic modelsContemporary Mathematics, 1989
- The linear abstract machineTheoretical Computer Science, 1988
- Algebraic TheoriesPublished by Springer Nature ,1976
- Call-by-name, call-by-value and the λ-calculusTheoretical Computer Science, 1975
- Strong functors and monoidal monadsArchiv der Mathematik, 1972