1 Search Results for "Knapp, Cory M."

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}
}
  • Refine by Author
  • 1 Escardó, Martín H.
  • 1 Knapp, Cory M.

  • Refine by Classification

  • Refine by Keyword
  • 1 computability theory
  • 1 dominance
  • 1 homotopy type theory
  • 1 partial function
  • 1 recursion theory
  • Show More...

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2017

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