Curry-style type isomorphisms and game semantics
| Autor: | Joachim De Lataillade |
|---|---|
| Přispěvatelé: | Preuves, Programmes et Systèmes (PPS), Centre National de la Recherche Scientifique (CNRS)-Université Paris Diderot - Paris 7 (UPD7) |
| Rok vydání: | 2008 |
| Předmět: |
FOS: Computer and information sciences
Computer Science - Logic in Computer Science Pure mathematics Game semantics 0102 computer and information sciences 01 natural sciences Mathematics (miscellaneous) Type isomorphisms Computer Science::Logic in Computer Science ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION Game Semantics 0101 mathematics Mathematics computer.programming_language Equational system System F 010102 general mathematics [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] Curry Curry-style system F Logic in Computer Science (cs.LO) Computer Science Applications TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES 010201 computation theory & mathematics TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Programming Languages F.3.2 ACM F.3.2 computer |
| Zdroj: | Mathematical Structures in Computer Science. 18:647-692 |
| ISSN: | 1469-8072 0960-1295 |
| DOI: | 10.1017/s0960129508006828 |
| Popis: | 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. Comment: Accept\'e \`a Mathematical Structures for Computer Science, Special Issue on Type Isomorphisms |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|