Game semantics for bounded polymorphism

James Laird

doi:10.1007/978-3-662-49630-5_4

Game semantics for bounded polymorphism

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

1 Citation (SciVal)

234 Downloads (Pure)

Abstract

We describe a denotational, intensional semantics for programs with polymorphic types with bounded quantification, in which phenomena such as inheritance between stateful objects may be represented and studied. Our model is developed from a game semantics for unbounded polymorphism, by establishing dinaturality properties of generic strategies, and using them to give a new construction for interpreting subtyping constraints and bounded quantification. We use this construction to give a denotational semantics for a programming language with general references and an expressive polymorphic typing system. We show that full abstraction fails in general in this model, but that it holds for all terms at a rich collection of bounded types.

Original language	English
Title of host publication	Foundations of Software Science and Computation Structures. FOSSACS 2016.
Subtitle of host publication	Proceedings of 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, Etaps 2016, Eindhoven, the Netherlands, April 2-8, 2016.
Editors	B. Jacobs, C. Loding
Place of Publication	The Netherlands
Publisher	Springer Verlag
Pages	55-70
Number of pages	16
ISBN (Print)	9783662496299
DOIs	https://doi.org/10.1007/978-3-662-49630-5_4
Publication status	Published - 22 Mar 2016
Event	19th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2016 and Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016 - Eindhoven, Netherlands Duration: 2 Apr 2016 → 8 Apr 2016

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	9634

Conference

Conference	19th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2016 and Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016
Country/Territory	Netherlands
City	Eindhoven
Period	2/04/16 → 8/04/16

Access to Document

10.1007/978-3-662-49630-5_4

fos16.pdf
The final publication is available at Springer via: http://dx.doi.org/10.1007/978-3-662-49630-5_4
Accepted author manuscript, 385 KB

Semantic Types for Verified Program Behaviour
Laird, J. (PI)
Engineering and Physical Sciences Research Council
28/02/14 → 31/07/17
Project: Research council

James Laird
- J.D.Lairdbath.acuk
- Department of Computer Science - Reader
- Mathematical Foundations of Computation
Person: Research & Teaching

Cite this

Laird, J. (2016). Game semantics for bounded polymorphism. In B. Jacobs, & C. Loding (Eds.), Foundations of Software Science and Computation Structures. FOSSACS 2016.: Proceedings of 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, Etaps 2016, Eindhoven, the Netherlands, April 2-8, 2016. (pp. 55-70). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9634). Springer Verlag. https://doi.org/10.1007/978-3-662-49630-5_4

Game semantics for bounded polymorphism. / Laird, James.
Foundations of Software Science and Computation Structures. FOSSACS 2016.: Proceedings of 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, Etaps 2016, Eindhoven, the Netherlands, April 2-8, 2016.. ed. / B. Jacobs; C. Loding. The Netherlands: Springer Verlag, 2016. p. 55-70 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9634).

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

Laird, J 2016, Game semantics for bounded polymorphism. in B Jacobs & C Loding (eds), Foundations of Software Science and Computation Structures. FOSSACS 2016.: Proceedings of 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, Etaps 2016, Eindhoven, the Netherlands, April 2-8, 2016.. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9634, Springer Verlag, The Netherlands, pp. 55-70, 19th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2016 and Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, Netherlands, 2/04/16. https://doi.org/10.1007/978-3-662-49630-5_4

Laird J. Game semantics for bounded polymorphism. In Jacobs B, Loding C, editors, Foundations of Software Science and Computation Structures. FOSSACS 2016.: Proceedings of 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, Etaps 2016, Eindhoven, the Netherlands, April 2-8, 2016.. The Netherlands: Springer Verlag. 2016. p. 55-70. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-662-49630-5_4

Laird, James. / Game semantics for bounded polymorphism. Foundations of Software Science and Computation Structures. FOSSACS 2016.: Proceedings of 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, Etaps 2016, Eindhoven, the Netherlands, April 2-8, 2016.. editor / B. Jacobs ; C. Loding. The Netherlands : Springer Verlag, 2016. pp. 55-70 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{35d86691efd745c591cee405bdba1361,

title = "Game semantics for bounded polymorphism",

abstract = "We describe a denotational, intensional semantics for programs with polymorphic types with bounded quantification, in which phenomena such as inheritance between stateful objects may be represented and studied. Our model is developed from a game semantics for unbounded polymorphism, by establishing dinaturality properties of generic strategies, and using them to give a new construction for interpreting subtyping constraints and bounded quantification. We use this construction to give a denotational semantics for a programming language with general references and an expressive polymorphic typing system. We show that full abstraction fails in general in this model, but that it holds for all terms at a rich collection of bounded types.",

author = "James Laird",

year = "2016",

month = mar,

day = "22",

doi = "10.1007/978-3-662-49630-5_4",

language = "English",

isbn = "9783662496299",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "55--70",

editor = "B. Jacobs and C. Loding",

booktitle = "Foundations of Software Science and Computation Structures. FOSSACS 2016.",

note = "19th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2016 and Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016 ; Conference date: 02-04-2016 Through 08-04-2016",

}

TY - GEN

T1 - Game semantics for bounded polymorphism

AU - Laird, James

PY - 2016/3/22

Y1 - 2016/3/22

N2 - We describe a denotational, intensional semantics for programs with polymorphic types with bounded quantification, in which phenomena such as inheritance between stateful objects may be represented and studied. Our model is developed from a game semantics for unbounded polymorphism, by establishing dinaturality properties of generic strategies, and using them to give a new construction for interpreting subtyping constraints and bounded quantification. We use this construction to give a denotational semantics for a programming language with general references and an expressive polymorphic typing system. We show that full abstraction fails in general in this model, but that it holds for all terms at a rich collection of bounded types.

AB - We describe a denotational, intensional semantics for programs with polymorphic types with bounded quantification, in which phenomena such as inheritance between stateful objects may be represented and studied. Our model is developed from a game semantics for unbounded polymorphism, by establishing dinaturality properties of generic strategies, and using them to give a new construction for interpreting subtyping constraints and bounded quantification. We use this construction to give a denotational semantics for a programming language with general references and an expressive polymorphic typing system. We show that full abstraction fails in general in this model, but that it holds for all terms at a rich collection of bounded types.

U2 - 10.1007/978-3-662-49630-5_4

DO - 10.1007/978-3-662-49630-5_4

M3 - Chapter in a published conference proceeding

AN - SCOPUS:84961732822

SN - 9783662496299

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 55

EP - 70

BT - Foundations of Software Science and Computation Structures. FOSSACS 2016.

A2 - Jacobs, B.

A2 - Loding, C.

PB - Springer Verlag

CY - The Netherlands

T2 - 19th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2016 and Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016

Y2 - 2 April 2016 through 8 April 2016

ER -

Game semantics for bounded polymorphism

Abstract

Publication series

Conference

Access to Document

Fingerprint

Projects

Semantic Types for Verified Program Behaviour

Profiles

James Laird

Cite this