Pierre Clairambault - 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 - https://doi.org/10.2168/LMCS-8(3:8)2012
Isomorphisms of types in the presence of higher-order references (extended version)

Authors: Pierre Clairambault

    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.


    Volume: Volume 8, Issue 3
    Published on: August 10, 2012
    Accepted on: June 25, 2015
    Submitted on: December 1, 2011
    Keywords: Computer Science - Logic in Computer Science,F.3.2

    2 Documents citing this article

    Share

    Consultation statistics

    This page has been seen 336 times.
    This article's PDF has been downloaded 166 times.