DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2019.33

Sequence Types for Hereditary Permutators

Authors: Pierre Vial

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

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.

Cite as

Pierre Vial. Sequence Types for Hereditary Permutators. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 33:1-33:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{vial:LIPIcs.FSCD.2019.33,
  author =	{Vial, Pierre},
  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 =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.33},
  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}
}

Document

DOI: 10.4230/LIPIcs.FSCD.2017.24

Types as Resources for Classical Natural Deduction

Authors: Delia Kesner and Pierre Vial

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

Abstract

We define two resource aware typing systems for the lambda-mu-calculus based on non-idempotent intersection and union types. The non-idempotent approach provides very simple combinatorial arguments - based on decreasing measures of type derivations - to characterize head and strongly normalizing terms. Moreover, typability provides upper bounds for the length of head-reduction sequences and maximal reduction sequences.

Cite as

Delia Kesner and Pierre Vial. Types as Resources for Classical Natural Deduction. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 24:1-24:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{kesner_et_al:LIPIcs.FSCD.2017.24,
  author =	{Kesner, Delia and Vial, Pierre},
  title =	{{Types as  Resources for Classical Natural Deduction}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{24:1--24:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.24},
  URN =		{urn:nbn:de:0030-drops-77135},
  doi =		{10.4230/LIPIcs.FSCD.2017.24},
  annote =	{Keywords: lambda-mu-calculus, classical logic, intersection types, normalization}
}

Search Results

Documents authored by Vial, Pierre

Sequence Types for Hereditary Permutators

Abstract

Cite as

Types as Resources for Classical Natural Deduction

Abstract

Cite as

Thanks for your feedback!

Could not send message