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.FSCD.2019.33
URN: urn:nbn:de:0030-drops-105404
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/10540/
Go to the corresponding LIPIcs Volume Portal

Vial, Pierre

Sequence Types for Hereditary Permutators

pdf-format:
LIPIcs-FSCD-2019-33.pdf (0.6 MB)

Abstract

The invertible terms in Scott's model D_infty are known as the hereditary permutators. Equivalently, they are terms which are invertible up to beta eta-conversion with respect to the composition of the lambda-terms. Finding a type-theoretic characterization to the set of hereditary permutators was problem # 20 of TLCA list of problems. In 2008, Tatsuta proved that this was not possible with an inductive type system. Building on previous work, we use an infinitary intersection type system based on sequences (i.e., families of types indexed by integers) to characterize hereditary permutators with a unique type. This gives a positive answer to the problem in the coinductive case.

BibTeX - Entry

@InProceedings{vial:LIPIcs:2019:10540,
  author =	{Pierre Vial},
  title =	{{Sequence Types for Hereditary Permutators}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{33:1--33:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Herman Geuvers},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/10540},
  URN =		{urn:nbn:de:0030-drops-105404},
  doi =		{10.4230/LIPIcs.FSCD.2019.33},
  annote =	{Keywords: hereditary permutators, B{\"o}hm trees, intersection types, coinduction, ridigity, sequence types, non-idempotent intersection}
}

Keywords: hereditary permutators, Böhm trees, intersection types, coinduction, ridigity, sequence types, non-idempotent intersection
Collection: 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
Issue Date: 2019
Date of publication: 18.06.2019

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