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 Dive into the research topics of 'Isomorphisms of types in the presence of higher-order references'. Together they form a unique fingerprint.

  • Projects

  • 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). IEEE. https://doi.org/10.1109/LICS.2011.32