Linearly Used Effects: Monadic and CPS Transformations into the Linear Lambda Calculus

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.

• Type: Conference
• Year: 2001
• Where: APLAS
• Authors: Masahito Hasegawa
• Keywords: APLAS 2001, Computational Lambda Calculus, Lambda Calculus, Linear Lambda Calculus, Programming Languages