1 Search Results for "Bos, Nathaniel"

Document
DOI: 10.4230/LIPIcs.TYPES.2019.9
Is Impredicativity Implicitly Implicit?

Authors: Stefan Monnier and Nathaniel Bos

Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)

Abstract
Of all the threats to the consistency of a type system, such as side effects and recursion, impredicativity is arguably the least understood. In this paper, we try to investigate it using a kind of blackbox reverse-engineering approach to map the landscape. We look at it with a particular focus on its interaction with the notion of implicit arguments, also known as erasable arguments. More specifically, we revisit several famous type systems believed to be consistent and which do include some form of impredicativity, and show that they can be refined to equivalent systems where impredicative quantification can be marked as erasable, in a stricter sense than the kind of proof irrelevance notion used for example for Prop terms in systems like Coq. We hope these observations will lead to a better understanding of why and when impredicativity can be sound. As a first step in this direction, we discuss how these results suggest some extensions of existing systems where constraining impredicativity to erasable quantifications might help preserve consistency.
Cite as

Stefan Monnier and Nathaniel Bos. Is Impredicativity Implicitly Implicit?. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{monnier_et_al:LIPIcs.TYPES.2019.9,
  author =	{Monnier, Stefan and Bos, Nathaniel},
  title =	{{Is Impredicativity Implicitly Implicit?}},
  booktitle =	{25th International Conference on Types for Proofs and Programs (TYPES 2019)},
  pages =	{9:1--9:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-158-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{175},
  editor =	{Bezem, Marc and Mahboubi, Assia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.9},
  URN =		{urn:nbn:de:0030-drops-130730},
  doi =		{10.4230/LIPIcs.TYPES.2019.9},
  annote =	{Keywords: Impredicativity, Pure type systems, Inductive types, Erasable arguments, Proof irrelevance, Implicit arguments, Universe polymorphism}
}
  • Refine by Author
  • 1 Bos, Nathaniel
  • 1 Monnier, Stefan

  • Refine by Classification
  • 1 Software and its engineering → Functional languages
  • 1 Theory of computation → Higher order logic
  • 1 Theory of computation → Type theory

  • Refine by Keyword
  • 1 Erasable arguments
  • 1 Implicit arguments
  • 1 Impredicativity
  • 1 Inductive types
  • 1 Proof irrelevance
  • Show More...

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2020

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