Isomorphisms of types in the presence of higher-order references

DOI10.2168/LMCS-8(3:8)2012zbMATH Open1256.68043arXiv1112.3198OpenAlexW2031775786MaRDI QIDQ2904625FDOQ2904625

Authors: Pierre Clairambault 

Publication date: 15 August 2012

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

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 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 this language with natural numbers.

Full work available at URL: https://arxiv.org/abs/1112.3198

Recommendations

• Publication:2769425
• On isomorphisms of intersection types
• On Isomorphisms of Intersection Types
• A short survey of isomorphisms of types
• Isomorphisms of simple inductive types through extensional rewriting
• Recursive properties of isomorphism types
• scientific article; zbMATH DE number 3869317
• Provable isomorphisms of types
• Remarks on isomorphisms of simple inductive types
• Mathematics of Program Construction

zbMATH Keywords

game semanticsgeneral referencesisomorphisms of types

Mathematics Subject Classification ID

Theory of programming languages (68N15) Graph theory (including graph drawing) in computer science (68R10) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Cited In (8)

• Automorphisms of types in certain type theories and representation of finite groups
• Second-order type isomorphisms through game semantics
• A short survey of isomorphisms of types
• Isomorphism of "Functional" Intersection Types
• Deconstructing general references via game semantics
• Title not available (Why is that?)
• Curry-style type isomorphisms and game semantics
• Foundations of dependent interoperability

This page was built for publication: Isomorphisms of types in the presence of higher-order references

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2904625)