Semantics of linear continuation-passing in call-by-name.
International Symposium on Functional and Logic Programming
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
Pointers to Related Work
Back to Hassei's
Research Page / Home Page