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)


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.

© Springer-Verlag 2004

[ps file] [pdf file]

Pointers to Related Work

Back to Hassei's Research Page / Home Page