DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2017.21

Partial Elements and Recursion via Dominances in Univalent Type Theory

Authors: Martín H. Escardó and Cory M. Knapp

Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

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.

Cite as

Martín H. Escardó and Cory M. Knapp. Partial Elements and Recursion via Dominances in Univalent Type Theory. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 21:1-21:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{escardo_et_al:LIPIcs.CSL.2017.21,
  author =	{Escard\'{o}, Mart{\'\i}n H. and Knapp, Cory M.},
  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 =	{Goranko, Valentin and Dam, Mads},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.21},
  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}
}

Search Results

Documents authored by Knapp, Cory M.

Partial Elements and Recursion via Dominances in Univalent Type Theory

Abstract

Cite as

Thanks for your feedback!

Could not send message