DROPS

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.2013.188

A Direct Version of Veldman's Proof of Open Induction on Cantor Space via Delimited Control Operators

Authors: Danko Ilik and Keiko Nakata

Published in: LIPIcs, Volume 26, 19th International Conference on Types for Proofs and Programs (TYPES 2013)

Abstract

First, we reconstruct Wim Veldman's result that Open Induction on Cantor space can be derived from Double-negation Shift and Markov's Principle. In doing this, we notice that one has to use a countable choice axiom in the proof and that Markov's Principle is replaceable by slightly strengthening the Double-negation Shift schema. We show that this strengthened version of Double-negation Shift can nonetheless be derived in a constructive intermediate logic based on delimited control operators, extended with axioms for higher-type Heyting Arithmetic. We formalize the argument and thus obtain a proof term that directly derives Open Induction on Cantor space by the shift and reset delimited control operators of Danvy and Filinski.

Cite as

Danko Ilik and Keiko Nakata. A Direct Version of Veldman's Proof of Open Induction on Cantor Space via Delimited Control Operators. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 188-201, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{ilik_et_al:LIPIcs.TYPES.2013.188,
  author =	{Ilik, Danko and Nakata, Keiko},
  title =	{{A Direct Version of Veldman's Proof of Open Induction on Cantor Space via Delimited Control Operators}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  pages =	{188--201},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Matthes, Ralph and Schubert, Aleksy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.188},
  URN =		{urn:nbn:de:0030-drops-46320},
  doi =		{10.4230/LIPIcs.TYPES.2013.188},
  annote =	{Keywords: Open Induction, Axiom of Choice, Double Negation Shift, Markov's Principle, delimited control operators}
}

Search Results

Documents authored by Nakata, Keiko

Realizability at Work: Separating Two Constructive Notions of Finiteness

Abstract

Cite as

A Direct Version of Veldman's Proof of Open Induction on Cantor Space via Delimited Control Operators

Abstract

Cite as

Thanks for your feedback!

Could not send message