Isomorphisms of types in the presence of higher-order references

Pierre Clairambault

Research output: Chapter in Book/Report/Conference proceedingChapter

1 Citation (Scopus)

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 languageEnglish
Title of host publication2011 IEEE 26th Annual Symposium on Logic in Computer Science
Place of PublicationPiscataway, NJ
PublisherIEEE
Pages152-161
Number of pages10
ISBN (Electronic)978-0-7695-4412-0
ISBN (Print) 978-1-4577-0451-2
DOIs
Publication statusPublished - 2011
Event26th Annual IEEE Symposium on Logic in Computer Science - Toronto, ON, Canada
Duration: 21 Jun 201124 Jun 2011

Conference

Conference26th Annual IEEE Symposium on Logic in Computer Science
Abbreviated titleLICS 2011
CountryCanada
CityToronto, ON
Period21/06/1124/06/11

Fingerprint

Isomorphism
Higher Order
Branching
Equational Theory
Natural number
Programming Languages
Deduce
Open Problems
Isomorphic
Game
If and only if
Model

Cite this

Clairambault, P. (2011). Isomorphisms of types in the presence of higher-order references. In 2011 IEEE 26th Annual Symposium on Logic in Computer Science (pp. 152-161). Piscataway, NJ: IEEE. https://doi.org/10.1109/LICS.2011.32

Isomorphisms of types in the presence of higher-order references. / Clairambault, Pierre.

2011 IEEE 26th Annual Symposium on Logic in Computer Science. Piscataway, NJ : IEEE, 2011. p. 152-161.

Research output: Chapter in Book/Report/Conference proceedingChapter

Clairambault, P 2011, Isomorphisms of types in the presence of higher-order references. in 2011 IEEE 26th Annual Symposium on Logic in Computer Science. IEEE, Piscataway, NJ, pp. 152-161, 26th Annual IEEE Symposium on Logic in Computer Science, Toronto, ON, Canada, 21/06/11. https://doi.org/10.1109/LICS.2011.32
Clairambault P. Isomorphisms of types in the presence of higher-order references. In 2011 IEEE 26th Annual Symposium on Logic in Computer Science. Piscataway, NJ: IEEE. 2011. p. 152-161 https://doi.org/10.1109/LICS.2011.32
Clairambault, Pierre. / Isomorphisms of types in the presence of higher-order references. 2011 IEEE 26th Annual Symposium on Logic in Computer Science. Piscataway, NJ : IEEE, 2011. pp. 152-161
@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",

}

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

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

ER -