2 Search Results for "Tranchini, Luca"

Document
DOI: 10.4230/LIPIcs.FSCD.2021.27
What’s Decidable About (Atomic) Polymorphism?

Authors: Paolo Pistone and Luca Tranchini

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
Due to the undecidability of most type-related properties of System F like type inhabitation or type checking, restricted polymorphic systems have been widely investigated (the most well-known being ML-polymorphism). In this paper we investigate System Fat, or atomic System F, a very weak predicative fragment of System F whose typable terms coincide with the simply typable ones. We show that the type-checking problem for Fat is decidable and we propose an algorithm which sheds some new light on the source of undecidability in full System F. Moreover, we investigate free theorems and contextual equivalence in this fragment, and we show that the latter, unlike in the simply typed lambda-calculus, is undecidable.
Cite as

Paolo Pistone and Luca Tranchini. What’s Decidable About (Atomic) Polymorphism?. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 27:1-27:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{pistone_et_al:LIPIcs.FSCD.2021.27,
  author =	{Pistone, Paolo and Tranchini, Luca},
  title =	{{What’s Decidable About (Atomic) Polymorphism?}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{27:1--27:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.27},
  URN =		{urn:nbn:de:0030-drops-142652},
  doi =		{10.4230/LIPIcs.FSCD.2021.27},
  annote =	{Keywords: Atomic System F, Predicative Polymorphism, ML-Polymorphism, Type-Checking, Contextual Equivalence, Free Theorems}
}
Document
DOI: 10.4230/LIPIcs.CSL.2021.35
The Yoneda Reduction of Polymorphic Types

Authors: Paolo Pistone and Luca Tranchini

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Abstract
In this paper we explore a family of type isomorphisms in System F whose validity corresponds, semantically, to some form of the Yoneda isomorphism from category theory. These isomorphisms hold under theories of equivalence stronger than βη-equivalence, like those induced by parametricity and dinaturality. We show that the Yoneda type isomorphisms yield a rewriting over types, that we call Yoneda reduction, which can be used to eliminate quantifiers from a polymorphic type, replacing them with a combination of monomorphic type constructors. We establish some sufficient conditions under which quantifiers can be fully eliminated from a polymorphic type, and we show some application of these conditions to count the inhabitants of a type and to compute program equivalence in some fragments of System F.
Cite as

Paolo Pistone and Luca Tranchini. The Yoneda Reduction of Polymorphic Types. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 35:1-35:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{pistone_et_al:LIPIcs.CSL.2021.35,
  author =	{Pistone, Paolo and Tranchini, Luca},
  title =	{{The Yoneda Reduction of Polymorphic Types}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{35:1--35:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.35},
  URN =		{urn:nbn:de:0030-drops-134696},
  doi =		{10.4230/LIPIcs.CSL.2021.35},
  annote =	{Keywords: System F, Type isomorphisms, Yoneda isomorphism, Program equivalence}
}
  • Refine by Author
  • 2 Pistone, Paolo
  • 2 Tranchini, Luca

  • Refine by Classification
  • 2 Theory of computation → Type theory
  • 1 Theory of computation → Higher order logic
  • 1 Theory of computation → Program semantics

  • Refine by Keyword
  • 1 Atomic System F
  • 1 Contextual Equivalence
  • 1 Free Theorems
  • 1 ML-Polymorphism
  • 1 Predicative Polymorphism
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 2 2021

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