Isomorphisms of types in the presence of higher-order references

Pierre Clairambault

doi:10.1109/LICS.2011.32

Isomorphisms of types in the presence of higher-order references

Pierre Clairambault

Department of Computer Science

Research output: Chapter or section in a book/report/conference proceeding › Chapter or section

2 Citations (SciVal)

Abstract

We investigate the problem of type isomorphisms in a programming language with higher-order references. We first recall the game-theoretic model of higher-order references by Abramsky, Honda and McCusker. Solving an open problem by Laurent, we show that two finitely branching arenas are isomorphic if and only if they are geometrically the same, up to renaming of moves (Laurent's forest isomorphism). We deduce from this an equational theory characterizing isomorphisms of types in a finitary language L2 with higher order references. We show however that Laurent's conjecture does not hold on infinitely branching arenas, yielding a non-trivial type isomorphism in the extension of L2 with natural numbers.

Original language	English
Title of host publication	2011 IEEE 26th Annual Symposium on Logic in Computer Science
Place of Publication	Piscataway, NJ
Publisher	IEEE
Pages	152-161
Number of pages	10
ISBN (Electronic)	978-0-7695-4412-0
ISBN (Print)	978-1-4577-0451-2
DOIs	https://doi.org/10.1109/LICS.2011.32
Publication status	Published - 2011
Event	26th Annual IEEE Symposium on Logic in Computer Science - Toronto, ON, Canada Duration: 21 Jun 2011 → 24 Jun 2011

Conference

Conference	26th Annual IEEE Symposium on Logic in Computer Science
Abbreviated title	LICS 2011
Country/Territory	Canada
City	Toronto, ON
Period	21/06/11 → 24/06/11

Access to Document

10.1109/LICS.2011.32

Cite this

@inbook{bd4677d4cf5d4ce881d6fa86a3ba1e05,

title = "Isomorphisms of types in the presence of higher-order references",

abstract = "We investigate the problem of type isomorphisms in a programming language with higher-order references. We first recall the game-theoretic model of higher-order references by Abramsky, Honda and McCusker. Solving an open problem by Laurent, we show that two finitely branching arenas are isomorphic if and only if they are geometrically the same, up to renaming of moves (Laurent's forest isomorphism). We deduce from this an equational theory characterizing isomorphisms of types in a finitary language L2 with higher order references. We show however that Laurent's conjecture does not hold on infinitely branching arenas, yielding a non-trivial type isomorphism in the extension of L2 with natural numbers.",

author = "Pierre Clairambault",

year = "2011",

doi = "10.1109/LICS.2011.32",

language = "English",

isbn = " 978-1-4577-0451-2",

pages = "152--161",

booktitle = "2011 IEEE 26th Annual Symposium on Logic in Computer Science",

publisher = "IEEE",

address = "USA United States",

note = "26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011 ; Conference date: 21-06-2011 Through 24-06-2011",

}

TY - CHAP

T1 - Isomorphisms of types in the presence of higher-order references

AU - Clairambault, Pierre

PY - 2011

Y1 - 2011

N2 - We investigate the problem of type isomorphisms in a programming language with higher-order references. We first recall the game-theoretic model of higher-order references by Abramsky, Honda and McCusker. Solving an open problem by Laurent, we show that two finitely branching arenas are isomorphic if and only if they are geometrically the same, up to renaming of moves (Laurent's forest isomorphism). We deduce from this an equational theory characterizing isomorphisms of types in a finitary language L2 with higher order references. We show however that Laurent's conjecture does not hold on infinitely branching arenas, yielding a non-trivial type isomorphism in the extension of L2 with natural numbers.

AB - We investigate the problem of type isomorphisms in a programming language with higher-order references. We first recall the game-theoretic model of higher-order references by Abramsky, Honda and McCusker. Solving an open problem by Laurent, we show that two finitely branching arenas are isomorphic if and only if they are geometrically the same, up to renaming of moves (Laurent's forest isomorphism). We deduce from this an equational theory characterizing isomorphisms of types in a finitary language L2 with higher order references. We show however that Laurent's conjecture does not hold on infinitely branching arenas, yielding a non-trivial type isomorphism in the extension of L2 with natural numbers.

UR - http://dx.doi.org/10.1109/LICS.2011.32

U2 - 10.1109/LICS.2011.32

DO - 10.1109/LICS.2011.32

M3 - Chapter or section

SN - 978-1-4577-0451-2

SP - 152

EP - 161

BT - 2011 IEEE 26th Annual Symposium on Logic in Computer Science

PB - IEEE

CY - Piscataway, NJ

T2 - 26th Annual IEEE Symposium on Logic in Computer Science

Y2 - 21 June 2011 through 24 June 2011

ER -

Isomorphisms of types in the presence of higher-order references

Abstract

Conference

Access to Document

Other files and links

Fingerprint

Semantic Structures for Higher-Order Information Flow

Cite this

Isomorphisms of types in the presence of higher-order references

Abstract

Conference

Access to Document

Other files and links

Fingerprint

Projects

Semantic Structures for Higher-Order Information Flow

Cite this