Linear logic, monads and the lambda calculus

N. Benton; P. Wadler

doi:10.1109/LICS.1996.561458

Linear logic, monads and the lambda calculus

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract / Description of output

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 language	English
Title of host publication	Logic in Computer Science, 1996. LICS '96. Proceedings., Eleventh Annual IEEE Symposium on
Pages	420 -431
DOIs	https://doi.org/10.1109/LICS.1996.561458
Publication status	Published - 1 Jul 1996

Access to Document

10.1109/LICS.1996.561458

Cite this

@inproceedings{e034a232e7a04cf78a72f25a9e422524,

title = "Linear logic, monads and the lambda calculus",

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",

author = "N. Benton and P. Wadler",

year = "1996",

month = jul,

day = "1",

doi = "10.1109/LICS.1996.561458",

language = "English",

isbn = "0-8186-7463-6",

pages = "420 --431",

booktitle = "Logic in Computer Science, 1996. LICS '96. Proceedings., Eleventh Annual IEEE Symposium on",

}

TY - GEN

T1 - Linear logic, monads and the lambda calculus

AU - Benton, N.

AU - Wadler, P.

PY - 1996/7/1

Y1 - 1996/7/1

N2 - 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

AB - 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

U2 - 10.1109/LICS.1996.561458

DO - 10.1109/LICS.1996.561458

M3 - Conference contribution

SN - 0-8186-7463-6

SP - 420

EP - 431

BT - Logic in Computer Science, 1996. LICS '96. Proceedings., Eleventh Annual IEEE Symposium on

ER -

Linear logic, monads and the lambda calculus

Abstract / Description of output

Access to Document

Fingerprint

Cite this