Linear logic, monads and the lambda calculus

N. Benton, P. Wadler

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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
Original languageEnglish
Title of host publicationLogic in Computer Science, 1996. LICS '96. Proceedings., Eleventh Annual IEEE Symposium on
Pages420 -431
DOIs
Publication statusPublished - 1 Jul 1996

Cite this