Computer Science – Logic in Computer Science
Scientific paper
2007-05-29
Computer Science
Logic in Computer Science
Accept\'e \`a Mathematical Structures for Computer Science, Special Issue on Type Isomorphisms
Scientific paper
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.
No associations
LandOfFree
Curry-style type Isomorphisms and Game Semantics does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Curry-style type Isomorphisms and Game Semantics, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Curry-style type Isomorphisms and Game Semantics will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-499368