Computational Lambda-Calculus and Monads

The λ-calculus is considered an useful mathematical tool in the study of programming languages. However, if one uses βη-conversion to prove equivalence of programs, then a gross simplification1 is introduced. We give 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.

• Type: Conference
• Year: 1989
• Where: LICS
• Authors: Eugenio Moggi
• Keywords: Automated Reasoning, Gross Simplification1, LICS 1989, Specific Computational Model, Useful Mathematical Tool