License: 
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
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://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7682/
Escardó, Martín H. ;
Knapp, Cory M.
Partial Elements and Recursion via Dominances in Univalent Type Theory
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 |
|
Collection: |
|
26th EACSL Annual Conference on Computer Science Logic (CSL 2017) |
|
Issue Date: |
|
2017 |
|
Date of publication: |
|
16.08.2017 |
