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