### Linearly used effects:
monadic and CPS transformations into the linear lambda calculus.

Masahito Hasegawa
In
*Proc. 6th
International Symposium on Functional and Logic Programming
(FLOPS2002)*,
Springer LNCS
2441 (2002) pages 167-182

### Abstract

We propose a semantic and syntactic framework for modelling
*linearly used effects*, by giving the monadic transforms
of the computational lambda calculus (considered as the core
calculus of typed call-by-value programming languages) into
the linear lambda calculus. As an instance Berdine et al.'s
work on *linearly used continuations* can be put in this
general picture. As a technical result we show the full completeness
of the CPS transform into the linear lambda calculus.
© Springer-Verlag 2002

### Pointers to Related Work

- A. Barber and
G. Plotkin,
**Dual Intuitionistic Linear Logic**.
Submitted for publication, 1997.
- J. Berdine,
P.W. O'Hearn,
U.S. Reddy and
H. Thielecke,
**Linearly used continuations**.
In *Proc. ACM SIGPLAN Workshop on Continuations (CW'01)*
(2001).
- N. Benton and P. Wadler,
**Linear logic, monads, and the lambda calculus**.
In *Proc. 11th Annual Symposium on Logic in Computer Science*
(1996) pp.420-431.
- M. Hasegawa,
**Girard translation and logical predicates**.
In *Journal of Functional Programming* 10(1) (2000) 77-89.
- M. Hasegawa,
**Classical linear logic of implications**.
In *Proc. Computer Science Logic*,
Springer LNCS 2471 (2002), pp.458-472.
- E. Moggi,
**Computational lambda-calculus and monads**.
In *Proc. 4th Annual Symposium on Logic in Computer Science*
(1989) pp.14-23.
- A. Sabry and M. Felleisen,
**Reasoning about programs in continuation-passing style**.
In *Proc. ACM Conference on Lisp and Functional Programming*
(1992) pp.288-298.

Back to Hassei's
Research Page / Home Page