2 Search Results for "Vial, Pierre"

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-dev.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-dev.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}
}
  • Refine by Author
  • 2 Vial, Pierre
  • 1 Kesner, Delia

  • Refine by Classification
  • 1 Theory of computation → Type theory

  • Refine by Keyword
  • 2 intersection types
  • 1 Böhm trees
  • 1 classical logic
  • 1 coinduction
  • 1 hereditary permutators
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2017
  • 1 2019

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact