Search Results

Documents authored by Parmann, Erik

Document
DOI: 10.4230/LIPIcs.TYPES.2016.6
Realizability at Work: Separating Two Constructive Notions of Finiteness

Authors: Marc Bezem, Thierry Coquand, Keiko Nakata, and Erik Parmann

Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)

Abstract
We elaborate in detail a realizability model for Martin-Löf dependent type theory with the purpose to analyze a subtle distinction between two constructive notions of finiteness of a set A. The two notions are: (1) A is Noetherian: the empty list can be constructed from lists over A containing duplicates by a certain inductive shortening process; (2) A is streamless: every enumeration of A contains a duplicate.
Cite as

Marc Bezem, Thierry Coquand, Keiko Nakata, and Erik Parmann. Realizability at Work: Separating Two Constructive Notions of Finiteness. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 6:1-6:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{bezem_et_al:LIPIcs.TYPES.2016.6,
  author =	{Bezem, Marc and Coquand, Thierry and Nakata, Keiko and Parmann, Erik},
  title =	{{Realizability at Work: Separating Two Constructive Notions of Finiteness}},
  booktitle =	{22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  pages =	{6:1--6:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.6},
  URN =		{urn:nbn:de:0030-drops-98541},
  doi =		{10.4230/LIPIcs.TYPES.2016.6},
  annote =	{Keywords: Type theory, realizability, constructive notions of finiteness}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2015.8
Functional Kan Simplicial Sets: Non-Constructivity of Exponentiation

Authors: Erik Parmann

Published in: LIPIcs, Volume 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018)

Abstract
Functional Kan simplicial sets are simplicial sets in which the horn-fillers required by the Kan extension condition are given explicitly by functions. We show the non-constructivity of the following basic result: if B and A are functional Kan simplicial sets, then A^B is a Kan simplicial set. This strengthens a similar result for the case of non-functional Kan simplicial sets shown by Bezem, Coquand and Parmann [TLCA 2015, v. 38 of LIPIcs]. Our result shows that-from a constructive point of view-functional Kan simplicial sets are, as it stands, unsatisfactory as a model of even simply typed lambda calculus. Our proof is based on a rather involved Kripke countermodel which has been encoded and verified in the Coq proof assistant.
Cite as

Erik Parmann. Functional Kan Simplicial Sets: Non-Constructivity of Exponentiation. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 8:1-8:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{parmann:LIPIcs.TYPES.2015.8,
  author =	{Parmann, Erik},
  title =	{{Functional Kan Simplicial Sets: Non-Constructivity of Exponentiation}},
  booktitle =	{21st International Conference on Types for Proofs and Programs (TYPES 2015)},
  pages =	{8:1--8:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-030-9},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{69},
  editor =	{Uustalu, Tarmo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.8},
  URN =		{urn:nbn:de:0030-drops-84787},
  doi =		{10.4230/LIPIcs.TYPES.2015.8},
  annote =	{Keywords: constructive logic, simplicial sets, semantics of simple types}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2014.187
Investigating Streamless Sets

Authors: Erik Parmann

Published in: LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)

Abstract
In this paper we look at streamless sets, recently investigated by Coquand and Spiwack. A set is streamless if every stream over that set contain a duplicate. It is an open question in constructive mathematics whether the Cartesian product of two streamless sets is streamless. We look at some settings in which the Cartesian product of two streamless sets is indeed streamless; in particular, we show that this holds in Martin-Loef intentional type theory when at least one of the sets have decidable equality. We go on to show that the addition of functional extensionality give streamless sets decidable equality, and then investigate these results in a few other constructive systems.
Cite as

Erik Parmann. Investigating Streamless Sets. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 187-201, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{parmann:LIPIcs.TYPES.2014.187,
  author =	{Parmann, Erik},
  title =	{{Investigating Streamless Sets}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{187--201},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.187},
  URN =		{urn:nbn:de:0030-drops-54971},
  doi =		{10.4230/LIPIcs.TYPES.2014.187},
  annote =	{Keywords: Type theory, Constructive Logic, Finite Sets}
}
Document
DOI: 10.4230/LIPIcs.TLCA.2015.92
Non-Constructivity in Kan Simplicial Sets

Authors: Marc Bezem, Thierry Coquand, and Erik Parmann

Published in: LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)

Abstract
We give an analysis of the non-constructivity of the following basic result: if X and Y are simplicial sets and Y has the Kan extension property, then Y^X also has the Kan extension property. By means of Kripke countermodels we show that even simple consequences of this basic result, such as edge reversal and edge composition, are not constructively provable. We also show that our unprovability argument will have to be refined if one strengthens the usual formulation of the Kan extension property to one with explicit horn-filler operations.
Cite as

Marc Bezem, Thierry Coquand, and Erik Parmann. Non-Constructivity in Kan Simplicial Sets. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 92-106, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{bezem_et_al:LIPIcs.TLCA.2015.92,
  author =	{Bezem, Marc and Coquand, Thierry and Parmann, Erik},
  title =	{{Non-Constructivity in Kan Simplicial Sets}},
  booktitle =	{13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
  pages =	{92--106},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-87-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{38},
  editor =	{Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.92},
  URN =		{urn:nbn:de:0030-drops-51579},
  doi =		{10.4230/LIPIcs.TLCA.2015.92},
  annote =	{Keywords: Constructive logic, simplicial sets, semantics of simple types}
}
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 About DROPS Imprint Privacy Contact