License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2013.129
URN: urn:nbn:de:0030-drops-46296
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2014/4629/
Go to the corresponding LIPIcs Volume Portal

Coppo, Mario ; Dezani-Ciancaglini, Mariangiola ; Margaria, Ines ; Zacchi, Maddalena

Isomorphism of "Functional" Intersection Types

pdf-format:
p129-07-coppo.pdf (0.6 MB)

Abstract

Type isomorphism for intersection types is quite odd, since it is not a congruence and it does not extend type equality in the standard interpretation of types. The lack of congruence is due to the proof theoretic nature of the intersection introduction rule, which requires the same term to be the subject of both premises. A partial congruence can be recovered by introducing a suitable notion of type similarity. Type equality in standard models becomes included in type isomorphism whenever atomic types have "functional" interpretations, i.e. they are equivalent to arrow types. This paper characterises type isomorphism for a type system in which the equivalence between atomic types and arrow types is induced by the initial projections of the Scott's model via the correspondence between inverse limit models and filter lambda-models.

BibTeX - Entry

@InProceedings{coppo_et_al:LIPIcs:2014:4629,
  author =	{Mario Coppo and Mariangiola Dezani-Ciancaglini and Ines Margaria and Maddalena Zacchi},
  title =	{{Isomorphism of "Functional" Intersection Types}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  pages =	{129--149},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Ralph Matthes and Aleksy Schubert},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2014/4629},
  URN =		{urn:nbn:de:0030-drops-46296},
  doi =		{10.4230/LIPIcs.TYPES.2013.129},
  annote =	{Keywords: Type Isomorphism, Lambda calculus, Intersection Types}
}

Keywords: Type Isomorphism, Lambda calculus, Intersection Types
Collection: 19th International Conference on Types for Proofs and Programs (TYPES 2013)
Issue Date: 2014
Date of publication: 25.07.2014

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI