Research

Isomorphisms of types in the presence of higher-order references


Reference:

Clairambault, P., 2011. Isomorphisms of types in the presence of higher-order references. In: 2011 IEEE 26th Annual Symposium on Logic in Computer Science. Piscataway, NJ: IEEE, pp. 152-161.

Related documents:

This repository does not currently have the full-text of this item.
You may be able to access a copy if URLs are provided below.

Official URL:

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

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.

Details

Item Type Book Sections
CreatorsClairambault, P.
DOI10.1109/LICS.2011.32
DepartmentsFaculty of Science > Computer Science
StatusPublished
ID Code25983
Additional Information26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011. 21-24 June 2011. Toronto, ON, Canada.

Export

Actions (login required)

View Item