Clairambault, Pierre - Isomorphisms of types in the presence of higher-order references (extended version)

lmcs:1040 - Logical Methods in Computer Science, August 10, 2012, Volume 8, Issue 3
Isomorphisms of types in the presence of higher-order references (extended version)

Authors: Clairambault, Pierre

We investigate the problem of type isomorphisms in the presence of higher-order references. We first introduce a finitary programming language with sum types and higher-order references, for which we build a fully abstract games model following the work of 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 our language. We show however that Laurent's conjecture does not hold on infinitely branching arenas, yielding new non-trivial type isomorphisms in a variant of our language with natural numbers.


Source : oai:arXiv.org:1207.3223
DOI : 10.2168/LMCS-8(3:8)2012
Volume: Volume 8, Issue 3
Published on: August 10, 2012
Submitted on: December 1, 2011
Keywords: Computer Science - Logic in Computer Science,F.3.2


Share

Consultation statistics

This page has been seen 44 times.
This article's PDF has been downloaded 16 times.