Eleventh Annual IEEE Symposium on

Logic in Computer Science (LICS 1996)

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

Authors: Nick Benton Philip Wadler


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.


    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}