Linear logic, monads and the lambda calculus
- 23 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 10436871,p. 420-431
- https://doi.org/10.1109/lics.1996.561458
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.Keywords
This publication has 10 references indexed in Scilit:
- Operational aspects of linear lambda calculusPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- State in HaskellHigher-Order and Symbolic Computation, 1995
- The ins and outs of Clean I/OJournal of Functional Programming, 1995
- The Girard Translation extended with recursionPublished by Springer Nature ,1995
- A syntax for linear logicPublished by Springer Nature ,1994
- New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logicInformation and Computation, 1992
- Comprehending monadsMathematical Structures in Computer Science, 1992
- Notions of computation and monadsInformation and Computation, 1991
- Linear logicTheoretical Computer Science, 1987
- Call-by-name, call-by-value and the λ-calculusTheoretical Computer Science, 1975