zbMATH — the first resource for mathematics

Semantics of linear continuation-passing in call-by-name. (English) Zbl 1122.68399
Kameyama, Yukiyoshi (ed.) et al., Functional and logic programming. 7th international symposium, FLOPS 2004, Nara, Japan, April 7–9, 2004. Proceedings. Berlin: Springer (ISBN 3-540-21402-X/pbk). Lecture Notes in Computer Science 2998, 229-243 (2004).
Summary: 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.
For the entire collection see [Zbl 1048.68005].
Reviewer: Reviewer (Berlin)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68N18 Functional programming and lambda calculus
68Q55 Semantics in the theory of computing
Full Text: DOI