## Paper: Linear Logic, Monads and the Lambda Calculus (at LICS 1996)

Authors:**Nick Benton Philip Wadler**

### 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.

### BibTeX

@InProceedings{BentonWadler-LinearLogicMonadsan, author = {Nick Benton and Philip Wadler}, title = {Linear Logic, Monads and the Lambda Calculus}, booktitle = {Proceedings of the Eleventh Annual IEEE Symp. on Logic in Computer Science, {LICS} 1996}, year = 1996, editor = {Edmund M. Clarke}, month = {July}, pages = {420-431}, location = {New Brunswick, NJ, USA}, publisher = {IEEE Computer Society Press} }