Curry-style type Isomorphisms and Game Semantics
| dc.creator | De Lataillade, Joachim | |
| dc.date | 2007-05-29 | |
| dc.date.accessioned | 2026-07-07T08:03:30Z | |
| dc.date.available | 2026-07-07T08:03:30Z | |
| dc.description | Curry-style system F, ie. system F with no explicit types in terms, can be seen as a core presentation of polymorphism from the point of view of programming languages. This paper gives a characterisation of type isomorphisms for this language, by using a game model whose intuitions come both from the syntax and from the game semantics universe. The model is composed of: an untyped part to interpret terms, a notion of game to interpret types, and a typed part to express the fact that an untyped strategy plays on a game. By analysing isomorphisms in the model, we prove that the equational system corresponding to type isomorphisms for Curry-style system F is the extension of the equational system for Church-style isomorphisms with a new, non-trivial equation: forall X.A = A[forall Y.Y/X] if X appears only positively in A. | |
| dc.description | Accepté à Mathematical Structures for Computer Science, Special Issue on Type Isomorphisms | |
| dc.identifier | https://arxiv.org/abs/0705.4228 | |
| dc.identifier | http://arxiv.org/abs/0705.4228 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/129603 | |
| dc.subject | Logic in Computer Science | |
| dc.subject | F.3.2 | |
| dc.title | Curry-style type Isomorphisms and Game Semantics | |
| dc.type | text |