License
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2017.21
URN: urn:nbn:de:0030-drops-76822
URL: http://drops.dagstuhl.de/opus/volltexte/2017/7682/
Go to the corresponding LIPIcs Volume Portal


Escardó, Martín H. ; Knapp, Cory M.

Partial Elements and Recursion via Dominances in Univalent Type Theory

pdf-format:
LIPIcs-CSL-2017-21.pdf (0.4 MB)


Abstract

We begin by revisiting partiality in univalent type theory via the notion of dominance. We then perform first steps in constructive computability theory, discussing the consequences of working with computability as property or structure, without assuming countable choice or Markov’s principle. A guiding question is what, if any, notion of partial function allows the proposition “all partial functions on natural numbers are Turing computable” to be consistent.

BibTeX - Entry

@InProceedings{escard_et_al:LIPIcs:2017:7682,
  author =	{Mart{\'i}n H. Escard{\'o} and Cory M. Knapp},
  title =	{{Partial Elements and Recursion via Dominances in Univalent Type Theory}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{21:1--21:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Valentin Goranko and Mads Dam},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7682},
  URN =		{urn:nbn:de:0030-drops-76822},
  doi =		{10.4230/LIPIcs.CSL.2017.21},
  annote =	{Keywords: univalent type theory, homotopy type theory, partial function, dominance, recursion theory, computability theory}
}

Keywords: univalent type theory, homotopy type theory, partial function, dominance, recursion theory, computability theory
Seminar: 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)
Issue Date: 2017
Date of publication: 14.08.2017


DROPS-Home | Fulltext Search | Imprint Published by LZI