A game semantics of linearly used continuations

James Laird

doi:10.1007/3-540-36576-1_20

A game semantics of linearly used continuations

James Laird

Research output: Chapter or section in a book/report/conference proceeding › Book chapter

7 Citations (SciVal)

Abstract

We present an analysis of the "linearly used continuation-passing 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 "well-bracketed" 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.

Original language	English
Title of host publication	Foundations of Software Science and Computation Structures
Subtitle of host publication	Proceedings of 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003 Warsaw, Poland, April 7–11, 2003
Editors	A. D. Gordon
Place of Publication	Berlin, Germany
Publisher	Springer Verlag
Pages	313-327
Number of pages	15
ISBN (Print)	9783540008972
DOIs	https://doi.org/10.1007/3-540-36576-1_20
Publication status	Published - 2003

Publication series

Name	Lecture Notes in Computer Science
Volume	2620

Access to Document

10.1007/3-540-36576-1_20

http://dx.doi.org/10.1007/3-540-36576-1_20

Cite this

Laird, J. (2003). A game semantics of linearly used continuations. In A. D. Gordon (Ed.), Foundations of Software Science and Computation Structures: Proceedings of 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003 Warsaw, Poland, April 7–11, 2003 (pp. 313-327). (Lecture Notes in Computer Science; Vol. 2620). Springer Verlag. https://doi.org/10.1007/3-540-36576-1_20

A game semantics of linearly used continuations. / Laird, James.
Foundations of Software Science and Computation Structures: Proceedings of 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003 Warsaw, Poland, April 7–11, 2003 . ed. / A. D. Gordon. Berlin, Germany: Springer Verlag, 2003. p. 313-327 (Lecture Notes in Computer Science; Vol. 2620).

Research output: Chapter or section in a book/report/conference proceeding › Book chapter

Laird, J 2003, A game semantics of linearly used continuations. in AD Gordon (ed.), Foundations of Software Science and Computation Structures: Proceedings of 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003 Warsaw, Poland, April 7–11, 2003 . Lecture Notes in Computer Science, vol. 2620, Springer Verlag, Berlin, Germany, pp. 313-327. https://doi.org/10.1007/3-540-36576-1_20

Laird J. A game semantics of linearly used continuations. In Gordon AD, editor, Foundations of Software Science and Computation Structures: Proceedings of 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003 Warsaw, Poland, April 7–11, 2003 . Berlin, Germany: Springer Verlag. 2003. p. 313-327. (Lecture Notes in Computer Science). doi: 10.1007/3-540-36576-1_20

Laird, James. / A game semantics of linearly used continuations. Foundations of Software Science and Computation Structures: Proceedings of 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003 Warsaw, Poland, April 7–11, 2003 . editor / A. D. Gordon. Berlin, Germany : Springer Verlag, 2003. pp. 313-327 (Lecture Notes in Computer Science).

@inbook{fb2c762b22f34fd7a1487f723a85321f,

title = "A game semantics of linearly used continuations",

abstract = "We present an analysis of the {"}linearly used continuation-passing 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 {"}well-bracketed{"} 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.",

author = "James Laird",

year = "2003",

doi = "10.1007/3-540-36576-1_20",

language = "English",

isbn = "9783540008972",

series = "Lecture Notes in Computer Science",

publisher = "Springer Verlag",

pages = "313--327",

editor = "Gordon, {A. D.}",

booktitle = "Foundations of Software Science and Computation Structures",

}

TY - CHAP

T1 - A game semantics of linearly used continuations

AU - Laird, James

PY - 2003

Y1 - 2003

N2 - We present an analysis of the "linearly used continuation-passing 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 "well-bracketed" 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.

AB - We present an analysis of the "linearly used continuation-passing 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 "well-bracketed" 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.

UR - http://www.scopus.com/inward/record.url?scp=21144435186&partnerID=8YFLogxK

UR - http://dx.doi.org/10.1007/3-540-36576-1_20

U2 - 10.1007/3-540-36576-1_20

DO - 10.1007/3-540-36576-1_20

M3 - Book chapter

AN - SCOPUS:21144435186

SN - 9783540008972

T3 - Lecture Notes in Computer Science

SP - 313

EP - 327

BT - Foundations of Software Science and Computation Structures

A2 - Gordon, A. D.

PB - Springer Verlag

CY - Berlin, Germany

ER -

A game semantics of linearly used continuations

Abstract

Publication series

Access to Document

Other files and links

Fingerprint

Cite this