Semantics of linear continuation-passing in call-by-name.

Masahito Hasegawa

In Proc. 7th International Symposium on Functional and Logic Programming (FLOPS2004), Springer LNCS 2998 (2004)

Abstract

We propose a semantic framework for modelling the linear usage of continuations in typed call-by-name programming languages. On the semantic side, we introduce a construction for categories of linear continuations, which gives rise to cartesian closed categories with ``linear classical disjunctions'' from models of intuitionistic linear logic with sums. On the syntactic side, we give a simply typed call-by-name lambda-mu-calculus in which the use of names (continuation variables) is restricted to be linear. Its semantic interpretation into a category of linear continuations then amounts to the call-by-name continuation-passing style (CPS) transformation into a linear lambda calculus with sum types. We show that our calculus is sound for this CPS semantics, hence for models given by the categories of linear continuations.

[ps file] [pdf file]

Pointers to Related Work

A. Barber and G. Plotkin, Dual intuitionistic linear logic. Manuscript, 1997.
J. Berdine, P.W. O'Hearn, U.S. Reddy and H. Thielecke, Linear continuation-passing. Higher-Order and Symbolic Computation 15(2/3) (2002) 181-203.
M. Hasegawa, Linearly used effects: monadic and CPS transformations into the linear lambda calculus. In Proc. FLOPS2002, Springer LNCS 2441 (2002) pp. 167-182.
P. Selinger, Control categories and duality: on the categorical semantics of the lambda-mu calculus. Math. Structures Comput. Sci. 11(2) (2001) 207-260.

Back to Hassei's Research Page / Home Page