Abstract
We present an analysis of the “linearly used continuationpassing interpretation” of functional languages, based on game semantics. This consists of a category of games with a coherence condition on moves —yielding a fully abstract model of an affine type-theory—and a syntax-independent and full embedding of a category of HO-style “wellbracketed” games into it. We show that this embedding corresponds precisely to linear CPS interpretation in its action on a games model of the call-by-value (untyped) λ-calculus, yielding a proof of full abstraction for the associated translation.
Notwithstanding the fact that, as emphasized in [6], “it is continuation transformers rather than the continuations which are linear” it seems reasonable to refer to a linear CPS interpretation, meaning a continuation-passing-interpretation based on linear types.
Chapter PDF
References
M. Abadi and M. P. Fiore. Syntactic considerations on recursive types. In Proceedings of the Eleventh Annual Symposium on Logic in Computer Science, LICS’ 96, 1996.
S. Abramsky. Axioms for full abstraction and full completeness. In Essays in Honour of Robin Milner. MIT Press, 1997.
S. Abramsky and G. McCusker. Call-by-value games. In M. Neilsen and W. Thomas, editors, Computer Science Logic: 11th Annual workshop proceedings, LNCS, pages 1–17. Springer-Verlag, 1998.
S. Abramsky, R. Jagadeesan and P. Malacaria. Full abstraction for PCF. Information and Computation, 163:409–470, 2000.
A. Barber. Dual intuitionistic linear logic. Technical Report ECS-LFCS-96-347, LFCS, University of Edinburgh, 1996.
Josh Berdine, Peter O'Hearn, Uday Reddy, and Hayo Thielecke. Linear continuation-passing. Higher Order Symbolic Computation, 15(2/3):181–208, September 2002.
Josh Berdine, Peter W. O'Hearn, and Hayo Thielecke. On affine typing and completeness of cps. Draft, December 2000.
C. Faggian and J. M. E. Hyland. Designs disputes and strategies. In Proccedings of CSL '02, 2002.
M. Hasegawa. Linearly used effects: monadic and cps transformations into the linear lambda calculus. In Proc. 6th International Symposium on Functional and Logic Programming (FLOPS2002), Aizu, number 2441 in LNCS, pages 167–182. Springer, 2002.
J. M. E. Hyland and C.-H. L. Ong. On full abstraction for PCF: I, II and III. Information and Computation, 163:285–408, 2000.
J. Laird. Full abstraction for functional languages with control. In Proceedings of the Twelfth International Symposium on Logic In Computer Science, LICS’ 97. IEEE Computer Society Press, 1997.
J. Laird. A Semantic Analysis of Control. PhD thesis, Department of Computer Science, University of Edinburgh, 1998.
J. Laird. Finite models and full completeness. In Proceedings of CSL’ 00, number 1862 in LNCS. Springer, 2000.
J. Laird. A fully abstract game semantics of local exceptions. In Proceedings of the Sixteenth International Symposium on Logic In Computer Science, LICS’ 01. IEEE Computer Society Press, 2001.
O. Laurent. Polarized games. In Proceedings of the Seventeenth International Symposium on Logic In Computer Science, LICS’ 02, 2002.
G. McCusker. Games and full abstraction for a functional metalanguage with recursive types. PhD thesis, Imperial College London, 1996.
A. M. Pitts. Relational properties of domains. Information and Computation, 127:66–90, 1996.
T. Streicher. A domain equation for the designs of Ludics. 2002.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Laird, J. (2003). A Game Semantics of Linearly Used Continuations. In: Gordon, A.D. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2003. Lecture Notes in Computer Science, vol 2620. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36576-1_20
Download citation
DOI: https://doi.org/10.1007/3-540-36576-1_20
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00897-2
Online ISBN: 978-3-540-36576-1
eBook Packages: Springer Book Archive