Access Restriction

Author Laird, J.
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©2013
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Polymorphism ♦ System F ♦ Full abstraction ♦ Game semantics ♦ Genericity ♦ References
Abstract This article presents a game semantics for higher-rank polymorphism, leading to a new model of the calculus System F, and a programming language which extends it with mutable variables. In contrast to previous game models of polymorphism, it is quite concrete, extending existing categories of games by a simple development of the notion of question/answer labelling and the associated bracketing condition to represent “copycat links” between positive and negative occurrences of type variables. Some well-known System F encodings of type constructors correspond in our model to simple constructions on games, such as the lifted sum. We characterize the $\textit{generic}$ types of our model (those for which instantiation reflects denotational equivalence), and show how to construct an interpretation in which all types are generic. We show how mutable variables (à la Scheme) may be interpreted in our model, allowing the definition of polymorphic objects with local state. By proving definability of finitary elements in this model using a decomposition argument, we establish a full abstraction result.
ISSN 00045411
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 2013-09-04
Publisher Place New York
e-ISSN 1557735X
Journal Journal of the ACM (JACM)
Volume Number 60
Issue Number 4
Page Count 27
Starting Page 1
Ending Page 27

Open content in new tab

   Open content in new tab
Source: ACM Digital Library