Lics

ACM/IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

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

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 Symposium on Logic in Computer Science (LICS 1996)},
    year =	 {1996},
    month =	 {July}, 
    pages =      {420--431},
    location =   {New Brunswick, NJ, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2022-10-3113:49
Sam Staton