Game semantics for call-by-value polymorphism
Reference:
Laird, J., 2010. Game semantics for call-by-value polymorphism. Lecture Notes in Computer Science, 6199 LNCS, pp. 187-198.
Related documents:
This repository does not currently have the full-text of this item.You may be able to access a copy if URLs are provided below. (Contact Author)
Official URL:
http://dx.doi.org/10.1007/978-3-642-14162-1_16
Related URLs:
Abstract
A game semantic approach to interpreting call-by-value polymorphism is described, based on extending Hyland-Ong games (which have already proved a rich source of models for higher-order programming languages with computational effects) with explicit "copycat links". This captures universal quantification in a simple and concrete way; it is effectively presentable, and opens the possibility of extending existing model checking techniques to polymorphic types. In particular, we present a fully abstract semantics for a call-by-value language with general references and full higher-rank polymorphism, within which polymorphic objects, for example, may be represented. We prove full abstraction by showing that every universally quantified type is a definable retract of its instantiation with the type of natural numbers.
Details
Item Type | Articles | ||||
Creators | Laird, J. | ||||
DOI | 10.1007/978-3-642-14162-1_16 | ||||
Related URLs |
| ||||
Departments | Faculty of Science > Computer Science | ||||
Refereed | No | ||||
Status | Published | ||||
ID Code | 20476 | ||||
Additional Information | AUTOMATA, LANGUAGES AND PROGRAMMING, PT II. 37th International Colloquium on Automata, Languages and Programming, ICALP 2010. 6-10 July 2010. Bordeaux, France. |
Export
Actions (login required)
View Item |