### 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.
© Springer-Verlag 2004

### Pointers to Related Work

Back to Hassei's
Research Page / Home Page