Linear logic, monads and the lambda calculus

authors: N Benton, P Wadler
year: 2002
url: https://ieeexplore.ieee.org/document/561458
publisher: IEEE Comput. Soc. Press
abstract: Models of intuitionistic linear logic also provide models of Moggi's computational metalanguage. We use the adjoint presentation of these models and the associated adjoint calculus to show that three translations, due mainly to Moggi, of the lambda calculus into the computational metalanguage (direct, call-by-name and call-by-value) correspond exactly to three translations, due mainly to Girard, of intuitionistic logic into intuitionistic linear logic. We also consider extending these results to languages with recursion.